From 123b9c7ea7088c78518eeae746de33011cd8b5a7 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Thu, 15 Jun 2023 15:55:28 +0200
Subject: [PATCH 01/31] Add a new type of VC for date computation program
 slicing

---
 compiler/verification/conditions.ml      | 49 +++++++++++++++++++++++-
 compiler/verification/conditions.mli     |  7 +++-
 compiler/verification/io.ml              | 14 +++++--
 compiler/verification/io.mli             |  7 ++--
 compiler/verification/solver.ml          | 26 +++++++++++--
 compiler/verification/z3backend.dummy.ml |  2 +-
 6 files changed, 91 insertions(+), 14 deletions(-)

diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 5687e44ad..f8922effb 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -289,9 +289,32 @@ let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) :
          e [])
       (Mark.get e)
 
+(** [slice_expression_for_date_computations ctx e] returns a list of
+    subexpressions of [e] whose top AST node is a computation on dates that can
+    raise [Dates_calc.AmbiguousComputation], that is [Dates_calc.add_dates]. The
+    list is ordered from the smallest subexpressions to the biggest. *)
+let rec slice_expression_for_date_computations (ctx : ctx) (e : typed expr) :
+    vc_return list =
+  match Mark.remove e with
+  | EApp
+      {
+        f =
+          EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound; tys = _ }, _;
+        args;
+      } ->
+    List.flatten (List.map (slice_expression_for_date_computations ctx) args)
+    @ [e]
+  | _ ->
+    Expr.shallow_fold
+      (fun e acc -> slice_expression_for_date_computations ctx e @ acc)
+      e []
+
 (** {1 Interface}*)
 
-type verification_condition_kind = NoEmptyError | NoOverlappingExceptions
+type verification_condition_kind =
+  | NoEmptyError
+  | NoOverlappingExceptions
+  | DateComputation
 
 type verification_condition = {
   vc_guard : typed expr;
@@ -384,6 +407,30 @@ let rec generate_verification_conditions_scope_body_expr
             :: vc_list
           | _ -> vc_list
         in
+        let vc_list =
+          let subexprs_dates : vc_return list =
+            slice_expression_for_date_computations ctx e
+          in
+          let subexprs_dates =
+            List.map
+              (fun e ->
+                if !Cli.optimize_flag then
+                  Expr.unbox (Shared_ast.Optimizations.optimize_expr ctx.decl e)
+                else e)
+              subexprs_dates
+          in
+          vc_list
+          @ List.map
+              (fun subexpr_date ->
+                {
+                  vc_guard = subexpr_date;
+                  vc_kind = DateComputation;
+                  vc_asserts = trivial_assert e;
+                  vc_scope = ctx.current_scope_name;
+                  vc_variable = scope_let_var, scope_let.scope_let_pos;
+                })
+              subexprs_dates
+        in
         ctx, vc_list, []
       | _ -> ctx, [], []
     in
diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli
index d38095448..e9e1f7396 100644
--- a/compiler/verification/conditions.mli
+++ b/compiler/verification/conditions.mli
@@ -23,10 +23,13 @@ open Shared_ast
 type verification_condition_kind =
   | NoEmptyError
       (** This verification condition checks whether a definition never returns
-          an empty error *)
+          an empty error. Has type [bool]. *)
   | NoOverlappingExceptions
       (** This verification condition checks whether a definition never returns
-          a conflict error *)
+          a conflict error. Has type [bool]. *)
+  | DateComputation
+      (** This verification condition is just a slice of the program (a
+          subexpression) that features computations on dates. *)
 
 type verification_condition = {
   vc_guard : typed Dcalc.Ast.expr;
diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index 69705e83f..e6217eb29 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -70,7 +70,7 @@ module type BackendIO = sig
     model option ->
     string
 
-  val encode_and_check_vc :
+  val check_vc :
     decl_ctx -> Conditions.verification_condition * vc_encoding_result -> bool
 end
 
@@ -113,6 +113,13 @@ module MakeBackendIO (B : Backend) = struct
           ScopeName.format_t vc.vc_scope
           (Bindlib.name_of (Mark.remove vc.vc_variable))
           Pos.format_loc_text (Mark.get vc.vc_variable)
+      | DateComputation ->
+        Format.asprintf
+          "@[<v>@{<yellow>[%a.%s]@} This date computation might be ambiguous:@,\
+           %a@]"
+          ScopeName.format_t vc.vc_scope
+          (Bindlib.name_of (Mark.remove vc.vc_variable))
+          Pos.format_loc_text (Expr.pos vc.vc_guard)
     in
     let counterexample : string option =
       if !Cli.disable_counterexamples then
@@ -139,7 +146,7 @@ module MakeBackendIO (B : Backend) = struct
     | None -> ""
     | Some counterexample -> "\n" ^ counterexample
 
-  let encode_and_check_vc
+  let check_vc
       (_decl_ctx : decl_ctx)
       (vc : Conditions.verification_condition * vc_encoding_result) : bool =
     let vc, z3_vc = vc in
@@ -154,7 +161,8 @@ module MakeBackendIO (B : Backend) = struct
       (match vc.vc_kind with
       | Conditions.NoEmptyError ->
         "the variable definition never to return an empty error"
-      | NoOverlappingExceptions -> "no two exceptions to ever overlap")
+      | NoOverlappingExceptions -> "no two exceptions to ever overlap"
+      | DateComputation -> "this date computation cannot be ambiguous")
       (Print.expr ()) vc.vc_guard (Print.expr ()) vc.vc_asserts;
 
     match z3_vc with
diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli
index 395733363..663291cfb 100644
--- a/compiler/verification/io.mli
+++ b/compiler/verification/io.mli
@@ -71,11 +71,10 @@ module type BackendIO = sig
     model option ->
     string
 
-  val encode_and_check_vc :
+  val check_vc :
     decl_ctx -> Conditions.verification_condition * vc_encoding_result -> bool
-  (** [encode_and_check_vc] spawns a new Z3 solver and tries to solve the
-      expression [vc]. Returns [true] if the vs was proven true and [false]
-      otherwise. **)
+  (** [check_vc] spawns a new Z3 solver and tries to solve the expression [vc].
+      Returns [true] if the vs was proven true and [false] otherwise. **)
 end
 
 module MakeBackendIO : functor (B : Backend) ->
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index d31791f78..10aeaa450 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -22,6 +22,21 @@ open Catala_utils
 let solve_vc
     (decl_ctx : Shared_ast.decl_ctx)
     (vcs : Conditions.verification_condition list) : unit =
+  let dates_vc =
+    List.filter
+      (fun vc ->
+        match vc.Conditions.vc_kind with
+        | Conditions.DateComputation -> true
+        | _ -> false)
+      vcs
+  in
+  List.iter
+    (fun dates_vc ->
+      Message.emit_result "%s"
+        (Z3backend.Io.print_negative_result dates_vc
+           (Z3backend.Io.make_context decl_ctx)
+           None))
+    dates_vc;
   (* Right now we only use the Z3 backend but the functorial interface should
      make it easy to mix and match different proof backends. *)
   Z3backend.Io.init_backend ();
@@ -39,13 +54,18 @@ let solve_vc
             in
             Z3backend.Io.Success (z3_vc, ctx)
           with Failure msg -> Fail msg ))
-      vcs
+      (List.filter
+         (fun vc ->
+           match vc.Conditions.vc_kind with
+           | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions ->
+             true
+           | Conditions.DateComputation -> false)
+         vcs)
   in
   let all_proven =
     List.fold_left
       (fun all_proven vc ->
-        if Z3backend.Io.encode_and_check_vc decl_ctx vc then all_proven
-        else false)
+        if Z3backend.Io.check_vc decl_ctx vc then all_proven else false)
       true z3_vcs
   in
   if all_proven then
diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml
index 7388fb75b..37bddf1a9 100644
--- a/compiler/verification/z3backend.dummy.ml
+++ b/compiler/verification/z3backend.dummy.ml
@@ -37,5 +37,5 @@ module Io = struct
   type vc_encoding_result = Success of model * model | Fail of string
 
   let print_negative_result _ _ _ = dummy ()
-  let encode_and_check_vc _ _ = dummy ()
+  let check_vc _ _ = dummy ()
 end

From 40a40fb88ed99b84b65ae5b1688b6e0cc70d650e Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Mon, 19 Jun 2023 14:07:34 +0200
Subject: [PATCH 02/31] Placeholder for scooping in variable values

---
 compiler/driver.ml                            |  3 +-
 compiler/verification/conditions.ml           | 67 +++++++------
 compiler/verification/conditions.mli          | 14 ++-
 compiler/verification/io.ml                   | 19 ++--
 compiler/verification/io.mli                  |  6 +-
 compiler/verification/solver.ml               | 96 ++++++++++---------
 compiler/verification/solver.mli              |  6 +-
 .../bad/array_length-empty.catala_en          |  2 +
 .../bad/array_length-overlap.catala_en        |  2 +
 tests/test_proof/bad/assert-empty.catala_en   |  2 +
 .../bad/dates_get_year-overlap.catala_en      |  2 +
 .../bad/dates_simple-empty.catala_en          |  2 +
 .../bad/dates_simple-overlap.catala_en        |  2 +
 tests/test_proof/bad/duration-empty.catala_en |  2 +
 .../test_proof/bad/duration-overlap.catala_en |  2 +
 tests/test_proof/bad/enums-empty.catala_en    |  2 +
 .../bad/enums-nonbool-empty.catala_en         |  2 +
 .../bad/enums-nonbool-overlap.catala_en       |  2 +
 tests/test_proof/bad/enums-overlap.catala_en  |  2 +
 .../test_proof/bad/enums_inj-empty.catala_en  |  2 +
 .../bad/enums_inj-overlap.catala_en           |  2 +
 .../test_proof/bad/enums_unit-empty.catala_en |  2 +
 .../bad/enums_unit-overlap.catala_en          |  2 +
 .../bad/let_in_condition-empty.catala_en      |  2 +
 tests/test_proof/bad/money-empty.catala_en    |  2 +
 tests/test_proof/bad/money-overlap.catala_en  |  2 +
 .../test_proof/bad/no_vars-conflict.catala_en |  2 +
 tests/test_proof/bad/no_vars-empty.catala_en  |  2 +
 .../test_proof/bad/rationals-empty.catala_en  |  2 +
 .../bad/rationals-overlap.catala_en           |  2 +
 tests/test_proof/bad/sat_solving.catala_en    |  2 +
 tests/test_proof/bad/structs-empty.catala_en  |  2 +
 .../test_proof/bad/structs-overlap.catala_en  |  2 +
 tests/test_proof/good/array_length.catala_en  |  2 +-
 tests/test_proof/good/assert.catala_en        |  2 +-
 .../test_proof/good/dates_get_year.catala_en  |  2 +-
 tests/test_proof/good/dates_simple.catala_en  |  2 +-
 .../good/direct_scope_call.catala_en          |  2 +-
 .../direct_scope_call_with_context.catala_en  |  2 +-
 tests/test_proof/good/duration.catala_en      |  2 +-
 tests/test_proof/good/enums-arith.catala_en   |  2 +-
 tests/test_proof/good/enums-nonbool.catala_en |  2 +-
 tests/test_proof/good/enums.catala_en         |  2 +-
 tests/test_proof/good/enums_inj.catala_en     |  2 +-
 tests/test_proof/good/enums_unit.catala_en    |  2 +-
 tests/test_proof/good/functions.catala_en     |  2 +-
 .../good/let_in_condition.catala_en           |  2 +-
 tests/test_proof/good/money.catala_en         |  2 +-
 tests/test_proof/good/no_vars.catala_en       |  2 +-
 tests/test_proof/good/rationals.catala_en     |  2 +-
 tests/test_proof/good/simple_vars.catala_en   |  2 +-
 tests/test_proof/good/structs.catala_en       |  2 +-
 52 files changed, 198 insertions(+), 103 deletions(-)

diff --git a/compiler/driver.ml b/compiler/driver.ml
index e910d90fc..ccdc1e5f7 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -370,8 +370,7 @@ let driver source_file (options : Cli.options) : int =
                 | None -> None
                 | Some _ -> Some scope_uid)
             in
-
-            Verification.Solver.solve_vc prgm.decl_ctx vcs
+            Verification.Solver.solve_vcs prgm.decl_ctx vcs
           | `Interpret ->
             Message.emit_debug "Starting interpretation (dcalc)...";
             let results =
diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index f8922effb..730697162 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -27,7 +27,6 @@ type vc_return = typed expr
 (** The return type of VC generators is the VC expression *)
 
 type ctx = {
-  current_scope_name : ScopeName.t;
   decl : decl_ctx;
   input_vars : typed expr Var.t list;
   scope_variables_typs : (typed expr, typ) Var.Map.t;
@@ -323,7 +322,6 @@ type verification_condition = {
   (* All assertions defined at the top-level of the scope corresponding to this
      assertion *)
   vc_asserts : typed expr;
-  vc_scope : ScopeName.t;
   vc_variable : typed expr Var.t Mark.pos;
 }
 
@@ -382,7 +380,6 @@ let rec generate_verification_conditions_scope_body_expr
               (* Placeholder until we add all assertions in scope once
                * we finished traversing it *)
               vc_asserts = trivial_assert e;
-              vc_scope = ctx.current_scope_name;
               vc_variable = scope_let_var, scope_let.scope_let_pos;
             };
           ]
@@ -401,7 +398,6 @@ let rec generate_verification_conditions_scope_body_expr
               vc_guard = Mark.copy e (Mark.remove vc_empty);
               vc_kind = NoEmptyError;
               vc_asserts = trivial_assert e;
-              vc_scope = ctx.current_scope_name;
               vc_variable = scope_let_var, scope_let.scope_let_pos;
             }
             :: vc_list
@@ -426,7 +422,6 @@ let rec generate_verification_conditions_scope_body_expr
                   vc_guard = subexpr_date;
                   vc_kind = DateComputation;
                   vc_asserts = trivial_assert e;
-                  vc_scope = ctx.current_scope_name;
                   vc_variable = scope_let_var, scope_let.scope_let_pos;
                 })
               subexprs_dates
@@ -446,14 +441,20 @@ let rec generate_verification_conditions_scope_body_expr
     in
     new_ctx, vc_list @ new_vcs, assert_list @ new_asserts
 
+type verification_conditions_scope = {
+  vc_scope_possible_variable_values :
+    (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
+  vc_scope_list : verification_condition list;
+}
+
 let generate_verification_conditions_code_items
     (decl_ctx : decl_ctx)
     (code_items : 'm expr code_item_list)
-    (s : ScopeName.t option) : verification_condition list =
+    (s : ScopeName.t option) : verification_conditions_scope ScopeName.Map.t =
   Scope.fold_left
-    ~f:(fun vcs item _ ->
+    ~f:(fun (vcs : verification_conditions_scope ScopeName.Map.t) item _ ->
       match item with
-      | Topdef _ -> []
+      | Topdef _ -> vcs
       | ScopeDef (name, body) ->
         let is_selected_scope =
           match s with
@@ -461,14 +462,13 @@ let generate_verification_conditions_code_items
           | None -> true
           | _ -> false
         in
-        let new_vcs =
-          if is_selected_scope then
+        if is_selected_scope then
+          let scope_vcs =
             let _scope_input_var, scope_body_expr =
               Bindlib.unbind body.scope_body_expr
             in
             let ctx =
               {
-                current_scope_name = name;
                 decl = decl_ctx;
                 input_vars = [];
                 scope_variables_typs =
@@ -489,24 +489,37 @@ let generate_verification_conditions_code_items
                    { pos = Pos.no_pos; ty = Mark.add Pos.no_pos (TLit TBool) })
             in
             List.map (fun vc -> { vc with vc_asserts = combined_assert }) vcs
-          else []
-        in
-        new_vcs @ vcs)
-    ~init:[] code_items
+          in
+          ScopeName.Map.add name
+            {
+              vc_scope_list = scope_vcs;
+              vc_scope_possible_variable_values =
+                Var.Map.empty (* TODO: implement that!*);
+            }
+            vcs
+        else vcs)
+    ~init:ScopeName.Map.empty code_items
 
 let generate_verification_conditions (p : 'm program) (s : ScopeName.t option) :
-    verification_condition list =
-  let vcs =
+    verification_conditions_scope ScopeName.Map.t =
+  let vcs : verification_conditions_scope ScopeName.Map.t =
     generate_verification_conditions_code_items p.decl_ctx p.code_items s
   in
-  (* We sort this list by scope name and then variable name to ensure consistent
-     output for testing*)
-  List.sort
-    (fun vc1 vc2 ->
-      let to_str vc =
-        Format.asprintf "%s.%s"
-          (Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
-          (Bindlib.name_of (Mark.remove vc.vc_variable))
-      in
-      String.compare (to_str vc1) (to_str vc2))
+  ScopeName.Map.mapi
+    (fun scope_name scope_vc ->
+      {
+        scope_vc with
+        vc_scope_list =
+          (* We sort this list by scope name and then variable name to ensure
+             consistent output for testing*)
+          List.sort
+            (fun vc1 vc2 ->
+              let to_str vc =
+                Format.asprintf "%s.%s"
+                  (Format.asprintf "%a" ScopeName.format_t scope_name)
+                  (Bindlib.name_of (Mark.remove vc.vc_variable))
+              in
+              String.compare (to_str vc1) (to_str vc2))
+            scope_vc.vc_scope_list;
+      })
     vcs
diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli
index e9e1f7396..edcd7b806 100644
--- a/compiler/verification/conditions.mli
+++ b/compiler/verification/conditions.mli
@@ -38,12 +38,22 @@ type verification_condition = {
   vc_asserts : typed Dcalc.Ast.expr;
       (** A conjunction of all assertions in scope of this VC. * This expression
           should have type [bool] *)
-  vc_scope : ScopeName.t;
   vc_variable : typed Dcalc.Ast.expr Var.t Mark.pos;
 }
 
+type verification_conditions_scope = {
+  vc_scope_possible_variable_values :
+    (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
+      (** For each variable, a list containing all the possible values that this
+          variable can have. This is a conservative analysis based on the
+          traversal of the default tree. *)
+  vc_scope_list : verification_condition list;
+}
+
 val generate_verification_conditions :
-  typed Dcalc.Ast.program -> ScopeName.t option -> verification_condition list
+  typed Dcalc.Ast.program ->
+  ScopeName.t option ->
+  verification_conditions_scope ScopeName.Map.t
 (** [generate_verification_conditions p None] will generate the verification
     conditions for all the variables of all the scopes of the program [p], while
     [generate_verification_conditions p (Some s)] will focus only on the
diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index e6217eb29..45b4ac1e1 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -66,12 +66,16 @@ module type BackendIO = sig
 
   val print_negative_result :
     Conditions.verification_condition ->
+    ScopeName.t ->
     backend_context ->
     model option ->
     string
 
   val check_vc :
-    decl_ctx -> Conditions.verification_condition * vc_encoding_result -> bool
+    decl_ctx ->
+    ScopeName.t ->
+    Conditions.verification_condition * vc_encoding_result ->
+    bool
 end
 
 module MakeBackendIO (B : Backend) = struct
@@ -94,6 +98,7 @@ module MakeBackendIO (B : Backend) = struct
 
   let print_negative_result
       (vc : Conditions.verification_condition)
+      (scope : ScopeName.t)
       (ctx : B.backend_context)
       (model : B.model option) : string =
     let var_and_pos =
@@ -102,7 +107,7 @@ module MakeBackendIO (B : Backend) = struct
         Format.asprintf
           "@[<v>@{<yellow>[%a.%s]@} This variable might return an empty error:@,\
            %a@]"
-          ScopeName.format_t vc.vc_scope
+          ScopeName.format_t scope
           (Bindlib.name_of (Mark.remove vc.vc_variable))
           Pos.format_loc_text (Mark.get vc.vc_variable)
       | Conditions.NoOverlappingExceptions ->
@@ -110,14 +115,14 @@ module MakeBackendIO (B : Backend) = struct
           "@[<v>@{<yellow>[%a.%s]@} At least two exceptions overlap for this \
            variable:@,\
            %a@]"
-          ScopeName.format_t vc.vc_scope
+          ScopeName.format_t scope
           (Bindlib.name_of (Mark.remove vc.vc_variable))
           Pos.format_loc_text (Mark.get vc.vc_variable)
       | DateComputation ->
         Format.asprintf
           "@[<v>@{<yellow>[%a.%s]@} This date computation might be ambiguous:@,\
            %a@]"
-          ScopeName.format_t vc.vc_scope
+          ScopeName.format_t scope
           (Bindlib.name_of (Mark.remove vc.vc_variable))
           Pos.format_loc_text (Expr.pos vc.vc_guard)
     in
@@ -148,6 +153,7 @@ module MakeBackendIO (B : Backend) = struct
 
   let check_vc
       (_decl_ctx : decl_ctx)
+      (scope : ScopeName.t)
       (vc : Conditions.verification_condition * vc_encoding_result) : bool =
     let vc, z3_vc = vc in
 
@@ -172,13 +178,14 @@ module MakeBackendIO (B : Backend) = struct
       match B.solve_vc_encoding backend_ctx encoding with
       | ProvenTrue -> true
       | ProvenFalse model ->
-        Message.emit_warning "%s" (print_negative_result vc backend_ctx model);
+        Message.emit_warning "%s"
+          (print_negative_result vc scope backend_ctx model);
         false
       | Unknown -> failwith "The solver failed at proving or disproving the VC")
     | Fail msg ->
       Message.emit_warning
         "@[<v>@{<yellow>[%a.%s]@} The translation to Z3 failed:@,%s@]"
-        ScopeName.format_t vc.vc_scope
+        ScopeName.format_t scope
         (Bindlib.name_of (Mark.remove vc.vc_variable))
         msg;
       false
diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli
index 663291cfb..636a8f3b6 100644
--- a/compiler/verification/io.mli
+++ b/compiler/verification/io.mli
@@ -67,12 +67,16 @@ module type BackendIO = sig
 
   val print_negative_result :
     Conditions.verification_condition ->
+    ScopeName.t ->
     backend_context ->
     model option ->
     string
 
   val check_vc :
-    decl_ctx -> Conditions.verification_condition * vc_encoding_result -> bool
+    decl_ctx ->
+    ScopeName.t ->
+    Conditions.verification_condition * vc_encoding_result ->
+    bool
   (** [check_vc] spawns a new Z3 solver and tries to solve the expression [vc].
       Returns [true] if the vs was proven true and [false] otherwise. **)
 end
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 10aeaa450..4091965f2 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -15,58 +15,66 @@
    the License. *)
 
 open Catala_utils
+open Shared_ast
 
 (** [solve_vc] is the main entry point of this module. It takes a list of
     expressions [vcs] corresponding to verification conditions that must be
     discharged by Z3, and attempts to solve them **)
-let solve_vc
+let solve_vcs
     (decl_ctx : Shared_ast.decl_ctx)
-    (vcs : Conditions.verification_condition list) : unit =
-  let dates_vc =
-    List.filter
-      (fun vc ->
-        match vc.Conditions.vc_kind with
-        | Conditions.DateComputation -> true
-        | _ -> false)
-      vcs
-  in
-  List.iter
-    (fun dates_vc ->
-      Message.emit_result "%s"
-        (Z3backend.Io.print_negative_result dates_vc
-           (Z3backend.Io.make_context decl_ctx)
-           None))
-    dates_vc;
+    (vcs : Conditions.verification_conditions_scope ScopeName.Map.t) : unit =
   (* Right now we only use the Z3 backend but the functorial interface should
      make it easy to mix and match different proof backends. *)
   Z3backend.Io.init_backend ();
-  let z3_vcs =
-    List.map
-      (fun vc ->
-        ( vc,
-          try
-            let ctx = Z3backend.Io.make_context decl_ctx in
-            let ctx =
-              Z3backend.Io.encode_asserts ctx vc.Conditions.vc_asserts
-            in
-            let ctx, z3_vc =
-              Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
-            in
-            Z3backend.Io.Success (z3_vc, ctx)
-          with Failure msg -> Fail msg ))
-      (List.filter
-         (fun vc ->
-           match vc.Conditions.vc_kind with
-           | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions ->
-             true
-           | Conditions.DateComputation -> false)
-         vcs)
-  in
   let all_proven =
-    List.fold_left
-      (fun all_proven vc ->
-        if Z3backend.Io.check_vc decl_ctx vc then all_proven else false)
-      true z3_vcs
+    ScopeName.Map.fold
+      (fun scope_name scope_vcs all_proven ->
+        let dates_vc =
+          List.filter
+            (fun vc ->
+              match vc.Conditions.vc_kind with
+              | Conditions.DateComputation -> true
+              | _ -> false)
+            scope_vcs.Conditions.vc_scope_list
+        in
+        List.iter
+          (fun dates_vc ->
+            Message.emit_result "%s"
+              (Z3backend.Io.print_negative_result dates_vc scope_name
+                 (Z3backend.Io.make_context decl_ctx)
+                 None))
+          dates_vc;
+        let z3_vcs =
+          List.map
+            (fun vc ->
+              ( vc,
+                try
+                  let ctx = Z3backend.Io.make_context decl_ctx in
+                  let ctx =
+                    Z3backend.Io.encode_asserts ctx vc.Conditions.vc_asserts
+                  in
+                  let ctx, z3_vc =
+                    Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
+                  in
+                  Z3backend.Io.Success (z3_vc, ctx)
+                with Failure msg -> Fail msg ))
+            (List.filter
+               (fun vc ->
+                 match vc.Conditions.vc_kind with
+                 | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
+                   ->
+                   true
+                 | Conditions.DateComputation -> false)
+               scope_vcs.Conditions.vc_scope_list)
+        in
+        List.fold_left
+          (fun all_proven vc ->
+            if Z3backend.Io.check_vc decl_ctx scope_name vc then all_proven
+            else false)
+          all_proven z3_vcs)
+      vcs true
   in
   if all_proven then
-    Message.emit_result "No errors found during the proof mode run."
+    Message.emit_result "No potential errors found during the proof mode run."
+  else
+    Message.raise_error "Some potential errors were found during the proof run."
diff --git a/compiler/verification/solver.mli b/compiler/verification/solver.mli
index 5ea951cbc..6014a7047 100644
--- a/compiler/verification/solver.mli
+++ b/compiler/verification/solver.mli
@@ -16,5 +16,7 @@
 
 (** Solves verification conditions using various proof backends *)
 
-val solve_vc :
-  Shared_ast.decl_ctx -> Conditions.verification_condition list -> unit
+val solve_vcs :
+  Shared_ast.decl_ctx ->
+  Conditions.verification_conditions_scope Shared_ast.ScopeName.Map.t ->
+  unit
diff --git a/tests/test_proof/bad/array_length-empty.catala_en b/tests/test_proof/bad/array_length-empty.catala_en
index 72066f257..5a0dd1043 100644
--- a/tests/test_proof/bad/array_length-empty.catala_en
+++ b/tests/test_proof/bad/array_length-empty.catala_en
@@ -19,4 +19,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/array_length-overlap.catala_en b/tests/test_proof/bad/array_length-overlap.catala_en
index 981b663ed..362f716ca 100644
--- a/tests/test_proof/bad/array_length-overlap.catala_en
+++ b/tests/test_proof/bad/array_length-overlap.catala_en
@@ -20,4 +20,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/assert-empty.catala_en b/tests/test_proof/bad/assert-empty.catala_en
index 870c662b0..b11bee855 100644
--- a/tests/test_proof/bad/assert-empty.catala_en
+++ b/tests/test_proof/bad/assert-empty.catala_en
@@ -31,4 +31,6 @@ $ catala Proof --disable_counterexamples
   │           ‾
 
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/dates_get_year-overlap.catala_en b/tests/test_proof/bad/dates_get_year-overlap.catala_en
index dca3c26ac..bf30d5fa6 100644
--- a/tests/test_proof/bad/dates_get_year-overlap.catala_en
+++ b/tests/test_proof/bad/dates_get_year-overlap.catala_en
@@ -22,4 +22,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/dates_simple-empty.catala_en b/tests/test_proof/bad/dates_simple-empty.catala_en
index 21c8ee2ed..7ae73aa8c 100644
--- a/tests/test_proof/bad/dates_simple-empty.catala_en
+++ b/tests/test_proof/bad/dates_simple-empty.catala_en
@@ -21,4 +21,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/dates_simple-overlap.catala_en b/tests/test_proof/bad/dates_simple-overlap.catala_en
index ad4952418..e68c193c0 100644
--- a/tests/test_proof/bad/dates_simple-overlap.catala_en
+++ b/tests/test_proof/bad/dates_simple-overlap.catala_en
@@ -22,4 +22,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/duration-empty.catala_en b/tests/test_proof/bad/duration-empty.catala_en
index ac710b8aa..88e5dcbef 100644
--- a/tests/test_proof/bad/duration-empty.catala_en
+++ b/tests/test_proof/bad/duration-empty.catala_en
@@ -19,4 +19,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/duration-overlap.catala_en b/tests/test_proof/bad/duration-overlap.catala_en
index e3bad00d6..ada9dff69 100644
--- a/tests/test_proof/bad/duration-overlap.catala_en
+++ b/tests/test_proof/bad/duration-overlap.catala_en
@@ -20,4 +20,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums-empty.catala_en b/tests/test_proof/bad/enums-empty.catala_en
index 81d1ca84a..5ed39b39a 100644
--- a/tests/test_proof/bad/enums-empty.catala_en
+++ b/tests/test_proof/bad/enums-empty.catala_en
@@ -37,4 +37,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums-nonbool-empty.catala_en b/tests/test_proof/bad/enums-nonbool-empty.catala_en
index 5e19edb3a..be42c044f 100644
--- a/tests/test_proof/bad/enums-nonbool-empty.catala_en
+++ b/tests/test_proof/bad/enums-nonbool-empty.catala_en
@@ -35,4 +35,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums-nonbool-overlap.catala_en b/tests/test_proof/bad/enums-nonbool-overlap.catala_en
index abf9f5610..820159750 100644
--- a/tests/test_proof/bad/enums-nonbool-overlap.catala_en
+++ b/tests/test_proof/bad/enums-nonbool-overlap.catala_en
@@ -35,4 +35,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums-overlap.catala_en b/tests/test_proof/bad/enums-overlap.catala_en
index 89e3ef2f9..f11a521e2 100644
--- a/tests/test_proof/bad/enums-overlap.catala_en
+++ b/tests/test_proof/bad/enums-overlap.catala_en
@@ -37,4 +37,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums_inj-empty.catala_en b/tests/test_proof/bad/enums_inj-empty.catala_en
index b6b2d602e..fce8d691c 100644
--- a/tests/test_proof/bad/enums_inj-empty.catala_en
+++ b/tests/test_proof/bad/enums_inj-empty.catala_en
@@ -30,4 +30,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Article
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums_inj-overlap.catala_en b/tests/test_proof/bad/enums_inj-overlap.catala_en
index 1f6bf5ae4..de3877804 100644
--- a/tests/test_proof/bad/enums_inj-overlap.catala_en
+++ b/tests/test_proof/bad/enums_inj-overlap.catala_en
@@ -25,4 +25,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Article
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums_unit-empty.catala_en b/tests/test_proof/bad/enums_unit-empty.catala_en
index 6a28690c0..a5af2ec56 100644
--- a/tests/test_proof/bad/enums_unit-empty.catala_en
+++ b/tests/test_proof/bad/enums_unit-empty.catala_en
@@ -28,4 +28,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Article
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/enums_unit-overlap.catala_en b/tests/test_proof/bad/enums_unit-overlap.catala_en
index 6e60e55b6..58c0ca6cc 100644
--- a/tests/test_proof/bad/enums_unit-overlap.catala_en
+++ b/tests/test_proof/bad/enums_unit-overlap.catala_en
@@ -28,4 +28,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Article
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/let_in_condition-empty.catala_en b/tests/test_proof/bad/let_in_condition-empty.catala_en
index 341e041eb..99b6057ee 100644
--- a/tests/test_proof/bad/let_in_condition-empty.catala_en
+++ b/tests/test_proof/bad/let_in_condition-empty.catala_en
@@ -20,4 +20,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/money-empty.catala_en b/tests/test_proof/bad/money-empty.catala_en
index 5de7fe034..e3b2e7669 100644
--- a/tests/test_proof/bad/money-empty.catala_en
+++ b/tests/test_proof/bad/money-empty.catala_en
@@ -23,4 +23,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/money-overlap.catala_en b/tests/test_proof/bad/money-overlap.catala_en
index aa60442be..2e41b0781 100644
--- a/tests/test_proof/bad/money-overlap.catala_en
+++ b/tests/test_proof/bad/money-overlap.catala_en
@@ -24,4 +24,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/no_vars-conflict.catala_en b/tests/test_proof/bad/no_vars-conflict.catala_en
index 178a790c8..e08f857f3 100644
--- a/tests/test_proof/bad/no_vars-conflict.catala_en
+++ b/tests/test_proof/bad/no_vars-conflict.catala_en
@@ -24,4 +24,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/no_vars-empty.catala_en b/tests/test_proof/bad/no_vars-empty.catala_en
index 6de8f1502..c6a640507 100644
--- a/tests/test_proof/bad/no_vars-empty.catala_en
+++ b/tests/test_proof/bad/no_vars-empty.catala_en
@@ -23,4 +23,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/rationals-empty.catala_en b/tests/test_proof/bad/rationals-empty.catala_en
index 528f013fa..ccaadfef3 100644
--- a/tests/test_proof/bad/rationals-empty.catala_en
+++ b/tests/test_proof/bad/rationals-empty.catala_en
@@ -19,4 +19,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/rationals-overlap.catala_en b/tests/test_proof/bad/rationals-overlap.catala_en
index 3f7a92ecb..df79de8f8 100644
--- a/tests/test_proof/bad/rationals-overlap.catala_en
+++ b/tests/test_proof/bad/rationals-overlap.catala_en
@@ -20,4 +20,6 @@ $ catala Proof --disable_counterexamples
   │          ‾
   └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/sat_solving.catala_en b/tests/test_proof/bad/sat_solving.catala_en
index 7b5ce646b..17e078f50 100644
--- a/tests/test_proof/bad/sat_solving.catala_en
+++ b/tests/test_proof/bad/sat_solving.catala_en
@@ -47,4 +47,6 @@ $ catala Proof --disable_counterexamples
    │          ‾‾‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/structs-empty.catala_en b/tests/test_proof/bad/structs-empty.catala_en
index 4f2b1cc09..d64b0f5c7 100644
--- a/tests/test_proof/bad/structs-empty.catala_en
+++ b/tests/test_proof/bad/structs-empty.catala_en
@@ -28,4 +28,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/bad/structs-overlap.catala_en b/tests/test_proof/bad/structs-overlap.catala_en
index 5bd9d0c48..587caa767 100644
--- a/tests/test_proof/bad/structs-overlap.catala_en
+++ b/tests/test_proof/bad/structs-overlap.catala_en
@@ -28,4 +28,6 @@ $ catala Proof --disable_counterexamples
    │          ‾
    └─ Test
 Counterexample generation is disabled so none was generated.
+[ERROR] Some potential errors were found during the proof run.
+#return code 255#
 ```
diff --git a/tests/test_proof/good/array_length.catala_en b/tests/test_proof/good/array_length.catala_en
index 55c4cb8a2..5f52ae6e0 100644
--- a/tests/test_proof/good/array_length.catala_en
+++ b/tests/test_proof/good/array_length.catala_en
@@ -13,5 +13,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/assert.catala_en b/tests/test_proof/good/assert.catala_en
index 9da9d222d..25c18e635 100644
--- a/tests/test_proof/good/assert.catala_en
+++ b/tests/test_proof/good/assert.catala_en
@@ -24,5 +24,5 @@ scope Foo:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/dates_get_year.catala_en b/tests/test_proof/good/dates_get_year.catala_en
index 4c2c385c1..bf99dfbdc 100644
--- a/tests/test_proof/good/dates_get_year.catala_en
+++ b/tests/test_proof/good/dates_get_year.catala_en
@@ -15,5 +15,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/dates_simple.catala_en b/tests/test_proof/good/dates_simple.catala_en
index 11b893c49..ef36b4a1e 100644
--- a/tests/test_proof/good/dates_simple.catala_en
+++ b/tests/test_proof/good/dates_simple.catala_en
@@ -15,5 +15,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/direct_scope_call.catala_en b/tests/test_proof/good/direct_scope_call.catala_en
index d5bf66230..a6f785d29 100644
--- a/tests/test_proof/good/direct_scope_call.catala_en
+++ b/tests/test_proof/good/direct_scope_call.catala_en
@@ -16,5 +16,5 @@ scope Foo:
 
 ```catala-test-inline
 $ catala Proof -s Foo
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/direct_scope_call_with_context.catala_en b/tests/test_proof/good/direct_scope_call_with_context.catala_en
index 583012492..9c6be8530 100644
--- a/tests/test_proof/good/direct_scope_call_with_context.catala_en
+++ b/tests/test_proof/good/direct_scope_call_with_context.catala_en
@@ -17,5 +17,5 @@ scope Foo:
 
 ```catala-test-inline
 $ catala Proof -s Foo
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/duration.catala_en b/tests/test_proof/good/duration.catala_en
index 01a2e840c..e6a8adfc8 100644
--- a/tests/test_proof/good/duration.catala_en
+++ b/tests/test_proof/good/duration.catala_en
@@ -13,5 +13,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums-arith.catala_en b/tests/test_proof/good/enums-arith.catala_en
index 4fe972ee8..a476035d5 100644
--- a/tests/test_proof/good/enums-arith.catala_en
+++ b/tests/test_proof/good/enums-arith.catala_en
@@ -28,5 +28,5 @@ $ catala Proof --disable_counterexamples
 5 │    -- C content boolean
   │       ‾
   └─ Test
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums-nonbool.catala_en b/tests/test_proof/good/enums-nonbool.catala_en
index 227d7d4e9..43c18ea7e 100644
--- a/tests/test_proof/good/enums-nonbool.catala_en
+++ b/tests/test_proof/good/enums-nonbool.catala_en
@@ -28,5 +28,5 @@ $ catala Proof --disable_counterexamples
 5 │    -- C content boolean
   │       ‾
   └─ Test
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums.catala_en b/tests/test_proof/good/enums.catala_en
index dbd08291c..5df85a17c 100644
--- a/tests/test_proof/good/enums.catala_en
+++ b/tests/test_proof/good/enums.catala_en
@@ -27,5 +27,5 @@ $ catala Proof --disable_counterexamples
 5 │    -- C content boolean
   │       ‾
   └─ Test
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums_inj.catala_en b/tests/test_proof/good/enums_inj.catala_en
index 4e2c7b46a..c9043f879 100644
--- a/tests/test_proof/good/enums_inj.catala_en
+++ b/tests/test_proof/good/enums_inj.catala_en
@@ -17,5 +17,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/enums_unit.catala_en b/tests/test_proof/good/enums_unit.catala_en
index d74268a25..27c120263 100644
--- a/tests/test_proof/good/enums_unit.catala_en
+++ b/tests/test_proof/good/enums_unit.catala_en
@@ -21,5 +21,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/functions.catala_en b/tests/test_proof/good/functions.catala_en
index c4de65b47..c8d05a1dd 100644
--- a/tests/test_proof/good/functions.catala_en
+++ b/tests/test_proof/good/functions.catala_en
@@ -14,5 +14,5 @@ scope A:
 ```
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/let_in_condition.catala_en b/tests/test_proof/good/let_in_condition.catala_en
index a37062d66..390319dbb 100644
--- a/tests/test_proof/good/let_in_condition.catala_en
+++ b/tests/test_proof/good/let_in_condition.catala_en
@@ -13,5 +13,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/money.catala_en b/tests/test_proof/good/money.catala_en
index 039fb1dda..a17563c9b 100644
--- a/tests/test_proof/good/money.catala_en
+++ b/tests/test_proof/good/money.catala_en
@@ -15,5 +15,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/no_vars.catala_en b/tests/test_proof/good/no_vars.catala_en
index 93244be96..ef9f0d445 100644
--- a/tests/test_proof/good/no_vars.catala_en
+++ b/tests/test_proof/good/no_vars.catala_en
@@ -10,5 +10,5 @@ scope A:
 ```
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/rationals.catala_en b/tests/test_proof/good/rationals.catala_en
index 11c66a408..1a3efbbff 100644
--- a/tests/test_proof/good/rationals.catala_en
+++ b/tests/test_proof/good/rationals.catala_en
@@ -13,5 +13,5 @@ scope A:
 
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/simple_vars.catala_en b/tests/test_proof/good/simple_vars.catala_en
index 211082b1a..a32a57fef 100644
--- a/tests/test_proof/good/simple_vars.catala_en
+++ b/tests/test_proof/good/simple_vars.catala_en
@@ -16,5 +16,5 @@ scope A:
 ```
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```
diff --git a/tests/test_proof/good/structs.catala_en b/tests/test_proof/good/structs.catala_en
index 30ae8e7de..a59226d7a 100644
--- a/tests/test_proof/good/structs.catala_en
+++ b/tests/test_proof/good/structs.catala_en
@@ -20,5 +20,5 @@ scope A:
 ```
 ```catala-test-inline
 $ catala Proof --disable_counterexamples 
-[RESULT] No errors found during the proof mode run.
+[RESULT] No potential errors found during the proof mode run.
 ```

From 1128c949f6b21ffc5c617caee766826827ac41d8 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Mon, 19 Jun 2023 14:59:25 +0200
Subject: [PATCH 03/31] Lift asserts to scope

---
 compiler/verification/conditions.ml  | 55 ++++++++++++----------------
 compiler/verification/conditions.mli |  6 +--
 compiler/verification/io.ml          |  4 +-
 compiler/verification/io.mli         |  1 +
 compiler/verification/solver.ml      |  5 ++-
 5 files changed, 33 insertions(+), 38 deletions(-)

diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 730697162..7c24672ff 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -319,9 +319,6 @@ type verification_condition = {
   vc_guard : typed expr;
   (* should have type bool *)
   vc_kind : verification_condition_kind;
-  (* All assertions defined at the top-level of the scope corresponding to this
-     assertion *)
-  vc_asserts : typed expr;
   vc_variable : typed expr Var.t Mark.pos;
 }
 
@@ -379,7 +376,6 @@ let rec generate_verification_conditions_scope_body_expr
               vc_kind = NoOverlappingExceptions;
               (* Placeholder until we add all assertions in scope once
                * we finished traversing it *)
-              vc_asserts = trivial_assert e;
               vc_variable = scope_let_var, scope_let.scope_let_pos;
             };
           ]
@@ -397,7 +393,6 @@ let rec generate_verification_conditions_scope_body_expr
             {
               vc_guard = Mark.copy e (Mark.remove vc_empty);
               vc_kind = NoEmptyError;
-              vc_asserts = trivial_assert e;
               vc_variable = scope_let_var, scope_let.scope_let_pos;
             }
             :: vc_list
@@ -421,7 +416,6 @@ let rec generate_verification_conditions_scope_body_expr
                 {
                   vc_guard = subexpr_date;
                   vc_kind = DateComputation;
-                  vc_asserts = trivial_assert e;
                   vc_variable = scope_let_var, scope_let.scope_let_pos;
                 })
               subexprs_dates
@@ -442,6 +436,7 @@ let rec generate_verification_conditions_scope_body_expr
     new_ctx, vc_list @ new_vcs, assert_list @ new_asserts
 
 type verification_conditions_scope = {
+  vc_scope_asserts : typed expr;
   vc_scope_possible_variable_values :
     (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
   vc_scope_list : verification_condition list;
@@ -463,35 +458,31 @@ let generate_verification_conditions_code_items
           | _ -> false
         in
         if is_selected_scope then
-          let scope_vcs =
-            let _scope_input_var, scope_body_expr =
-              Bindlib.unbind body.scope_body_expr
-            in
-            let ctx =
-              {
-                decl = decl_ctx;
-                input_vars = [];
-                scope_variables_typs =
-                  Var.Map.empty
-                  (* We don't need to add the typ of the scope input var here
-                     because it will never appear in an expression for which we
-                     generate a verification conditions (the big struct is
-                     destructured with a series of let bindings just after. )*);
-              }
-            in
-            let _, vcs, asserts =
-              generate_verification_conditions_scope_body_expr ctx
-                scope_body_expr
-            in
-            let combined_assert =
-              conjunction_exprs asserts
-                (Typed
-                   { pos = Pos.no_pos; ty = Mark.add Pos.no_pos (TLit TBool) })
-            in
-            List.map (fun vc -> { vc with vc_asserts = combined_assert }) vcs
+          let _scope_input_var, scope_body_expr =
+            Bindlib.unbind body.scope_body_expr
+          in
+          let ctx =
+            {
+              decl = decl_ctx;
+              input_vars = [];
+              scope_variables_typs =
+                Var.Map.empty
+                (* We don't need to add the typ of the scope input var here
+                   because it will never appear in an expression for which we
+                   generate a verification conditions (the big struct is
+                   destructured with a series of let bindings just after. )*);
+            }
+          in
+          let _, scope_vcs, asserts =
+            generate_verification_conditions_scope_body_expr ctx scope_body_expr
+          in
+          let combined_assert =
+            conjunction_exprs asserts
+              (Typed { pos = Pos.no_pos; ty = Mark.add Pos.no_pos (TLit TBool) })
           in
           ScopeName.Map.add name
             {
+              vc_scope_asserts = combined_assert;
               vc_scope_list = scope_vcs;
               vc_scope_possible_variable_values =
                 Var.Map.empty (* TODO: implement that!*);
diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli
index edcd7b806..1525c413d 100644
--- a/compiler/verification/conditions.mli
+++ b/compiler/verification/conditions.mli
@@ -35,13 +35,13 @@ type verification_condition = {
   vc_guard : typed Dcalc.Ast.expr;
       (** This expression should have type [bool]*)
   vc_kind : verification_condition_kind;
-  vc_asserts : typed Dcalc.Ast.expr;
-      (** A conjunction of all assertions in scope of this VC. * This expression
-          should have type [bool] *)
   vc_variable : typed Dcalc.Ast.expr Var.t Mark.pos;
 }
 
 type verification_conditions_scope = {
+  vc_scope_asserts : typed Dcalc.Ast.expr;
+      (** A conjunction of all assertions in scope. This expression should have
+          type [bool] *)
   vc_scope_possible_variable_values :
     (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
       (** For each variable, a list containing all the possible values that this
diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index 45b4ac1e1..6fbadd28a 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -74,6 +74,7 @@ module type BackendIO = sig
   val check_vc :
     decl_ctx ->
     ScopeName.t ->
+    Conditions.verification_conditions_scope ->
     Conditions.verification_condition * vc_encoding_result ->
     bool
 end
@@ -154,6 +155,7 @@ module MakeBackendIO (B : Backend) = struct
   let check_vc
       (_decl_ctx : decl_ctx)
       (scope : ScopeName.t)
+      (vc_scope_ctx : Conditions.verification_conditions_scope)
       (vc : Conditions.verification_condition * vc_encoding_result) : bool =
     let vc, z3_vc = vc in
 
@@ -169,7 +171,7 @@ module MakeBackendIO (B : Backend) = struct
         "the variable definition never to return an empty error"
       | NoOverlappingExceptions -> "no two exceptions to ever overlap"
       | DateComputation -> "this date computation cannot be ambiguous")
-      (Print.expr ()) vc.vc_guard (Print.expr ()) vc.vc_asserts;
+      (Print.expr ()) vc.vc_guard (Print.expr ()) vc_scope_ctx.vc_scope_asserts;
 
     match z3_vc with
     | Success (encoding, backend_ctx) -> (
diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli
index 636a8f3b6..a9b9559bf 100644
--- a/compiler/verification/io.mli
+++ b/compiler/verification/io.mli
@@ -75,6 +75,7 @@ module type BackendIO = sig
   val check_vc :
     decl_ctx ->
     ScopeName.t ->
+    Conditions.verification_conditions_scope ->
     Conditions.verification_condition * vc_encoding_result ->
     bool
   (** [check_vc] spawns a new Z3 solver and tries to solve the expression [vc].
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 4091965f2..a58e05b68 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -51,7 +51,7 @@ let solve_vcs
                 try
                   let ctx = Z3backend.Io.make_context decl_ctx in
                   let ctx =
-                    Z3backend.Io.encode_asserts ctx vc.Conditions.vc_asserts
+                    Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
                   in
                   let ctx, z3_vc =
                     Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
@@ -69,7 +69,8 @@ let solve_vcs
         in
         List.fold_left
           (fun all_proven vc ->
-            if Z3backend.Io.check_vc decl_ctx scope_name vc then all_proven
+            if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
+              all_proven
             else false)
           all_proven z3_vcs)
       vcs true

From d23c0e2d0e2f2c98486ce4aa3079a726d37696ef Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Mon, 19 Jun 2023 15:07:20 +0200
Subject: [PATCH 04/31] Inside ctx rather than a returned list

---
 compiler/verification/conditions.ml | 80 +++++++++++++++++------------
 1 file changed, 47 insertions(+), 33 deletions(-)

diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 7c24672ff..c42fb01dc 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -26,10 +26,11 @@ open Ast
 type vc_return = typed expr
 (** The return type of VC generators is the VC expression *)
 
-type ctx = {
-  decl : decl_ctx;
-  input_vars : typed expr Var.t list;
-  scope_variables_typs : (typed expr, typ) Var.Map.t;
+type scope_conditions_ctx = {
+  scope_cond_decls : decl_ctx;
+  scope_cond_input_vars : typed expr Var.t list;
+  scope_cond_variables_typs : (typed expr, typ) Var.Map.t;
+  scope_cond_asserts : typed expr list;
 }
 
 let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) :
@@ -110,8 +111,9 @@ let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list =
     variables, or [fun () -> e1] for subscope variables. But what we really want
     to analyze is only [e1], so we match this outermost structure explicitely
     and have a clean verification condition generator that only runs on [e1] *)
-let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
-    typed expr =
+let match_and_ignore_outer_reentrant_default
+    (ctx : scope_conditions_ctx)
+    (e : typed expr) : typed expr =
   match Mark.remove e with
   | EErrorOnEmpty
       ( EDefault
@@ -121,7 +123,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
             cons;
           },
         _ )
-    when List.exists (fun x' -> Var.eq x x') ctx.input_vars ->
+    when List.exists (fun x' -> Var.eq x x') ctx.scope_cond_input_vars ->
     (* scope variables*)
     cons
   | EAbs { binder; tys = [(TLit TUnit, _)] } ->
@@ -154,8 +156,9 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
     [b] such that if [b] is true, then [e] will never return an empty error. It
     also returns a map of all the types of locally free variables inside the
     expression. *)
-let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
-    vc_return =
+let rec generate_vc_must_not_return_empty
+    (ctx : scope_conditions_ctx)
+    (e : typed expr) : vc_return =
   match Mark.remove e with
   | EAbs { binder; _ } ->
     (* Hot take: for a function never to return an empty error when called, it
@@ -246,8 +249,9 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
     expression [b] such that if [b] is true, then [e] will never return a
     conflict error. It also returns a map of all the types of locally free
     variables inside the expression. *)
-let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) :
-    vc_return =
+let rec generate_vc_must_not_return_conflict
+    (ctx : scope_conditions_ctx)
+    (e : typed expr) : vc_return =
   (* See the code of [generate_vc_must_not_return_empty] for a list of
      invariants on which this function relies on. *)
   match Mark.remove e with
@@ -292,8 +296,9 @@ let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) :
     subexpressions of [e] whose top AST node is a computation on dates that can
     raise [Dates_calc.AmbiguousComputation], that is [Dates_calc.add_dates]. The
     list is ordered from the smallest subexpressions to the biggest. *)
-let rec slice_expression_for_date_computations (ctx : ctx) (e : typed expr) :
-    vc_return list =
+let rec slice_expression_for_date_computations
+    (ctx : scope_conditions_ctx)
+    (e : typed expr) : vc_return list =
   match Mark.remove e with
   | EApp
       {
@@ -325,16 +330,16 @@ type verification_condition = {
 let trivial_assert e = Mark.copy e (ELit (LBool true))
 
 let rec generate_verification_conditions_scope_body_expr
-    (ctx : ctx)
+    (ctx : scope_conditions_ctx)
     (scope_body_expr : 'm expr scope_body_expr) :
-    ctx * verification_condition list * typed expr list =
+    scope_conditions_ctx * verification_condition list =
   match scope_body_expr with
-  | Result _ -> ctx, [], []
+  | Result _ -> ctx, []
   | ScopeLet scope_let ->
     let scope_let_var, scope_let_next =
       Bindlib.unbind scope_let.scope_let_next
     in
-    let new_ctx, vc_list, assert_list =
+    let new_ctx, vc_list =
       match scope_let.scope_let_kind with
       | Assertion -> (
         let e =
@@ -343,7 +348,7 @@ let rec generate_verification_conditions_scope_body_expr
         match Mark.remove e with
         | EAssert e ->
           let e = match_and_ignore_outer_reentrant_default ctx e in
-          ctx, [], [e]
+          { ctx with scope_cond_asserts = e :: ctx.scope_cond_asserts }, []
         | _ ->
           Message.raise_spanned_error (Expr.pos e)
             "Internal error: this assertion does not have the structure \
@@ -351,7 +356,11 @@ let rec generate_verification_conditions_scope_body_expr
              %a"
             (Print.expr ()) e)
       | DestructuringInputStruct ->
-        { ctx with input_vars = scope_let_var :: ctx.input_vars }, [], []
+        ( {
+            ctx with
+            scope_cond_input_vars = scope_let_var :: ctx.scope_cond_input_vars;
+          },
+          [] )
       | ScopeVarDefinition | SubScopeVarDefinition ->
         (* For scope variables, we should check both that they never evaluate to
            emptyError nor conflictError. But for subscope variable definitions,
@@ -366,7 +375,8 @@ let rec generate_verification_conditions_scope_body_expr
         let vc_confl =
           if !Cli.optimize_flag then
             Expr.unbox
-              (Shared_ast.Optimizations.optimize_expr ctx.decl vc_confl)
+              (Shared_ast.Optimizations.optimize_expr ctx.scope_cond_decls
+                 vc_confl)
           else vc_confl
         in
         let vc_list =
@@ -387,7 +397,8 @@ let rec generate_verification_conditions_scope_body_expr
             let vc_empty =
               if !Cli.optimize_flag then
                 Expr.unbox
-                  (Shared_ast.Optimizations.optimize_expr ctx.decl vc_empty)
+                  (Shared_ast.Optimizations.optimize_expr ctx.scope_cond_decls
+                     vc_empty)
               else vc_empty
             in
             {
@@ -406,7 +417,9 @@ let rec generate_verification_conditions_scope_body_expr
             List.map
               (fun e ->
                 if !Cli.optimize_flag then
-                  Expr.unbox (Shared_ast.Optimizations.optimize_expr ctx.decl e)
+                  Expr.unbox
+                    (Shared_ast.Optimizations.optimize_expr ctx.scope_cond_decls
+                       e)
                 else e)
               subexprs_dates
           in
@@ -420,20 +433,20 @@ let rec generate_verification_conditions_scope_body_expr
                 })
               subexprs_dates
         in
-        ctx, vc_list, []
-      | _ -> ctx, [], []
+        ctx, vc_list
+      | _ -> ctx, []
     in
-    let new_ctx, new_vcs, new_asserts =
+    let new_ctx, new_vcs =
       generate_verification_conditions_scope_body_expr
         {
           new_ctx with
-          scope_variables_typs =
+          scope_cond_variables_typs =
             Var.Map.add scope_let_var scope_let.scope_let_typ
-              new_ctx.scope_variables_typs;
+              new_ctx.scope_cond_variables_typs;
         }
         scope_let_next
     in
-    new_ctx, vc_list @ new_vcs, assert_list @ new_asserts
+    new_ctx, vc_list @ new_vcs
 
 type verification_conditions_scope = {
   vc_scope_asserts : typed expr;
@@ -463,9 +476,10 @@ let generate_verification_conditions_code_items
           in
           let ctx =
             {
-              decl = decl_ctx;
-              input_vars = [];
-              scope_variables_typs =
+              scope_cond_decls = decl_ctx;
+              scope_cond_asserts = [];
+              scope_cond_input_vars = [];
+              scope_cond_variables_typs =
                 Var.Map.empty
                 (* We don't need to add the typ of the scope input var here
                    because it will never appear in an expression for which we
@@ -473,11 +487,11 @@ let generate_verification_conditions_code_items
                    destructured with a series of let bindings just after. )*);
             }
           in
-          let _, scope_vcs, asserts =
+          let ctx, scope_vcs =
             generate_verification_conditions_scope_body_expr ctx scope_body_expr
           in
           let combined_assert =
-            conjunction_exprs asserts
+            conjunction_exprs ctx.scope_cond_asserts
               (Typed { pos = Pos.no_pos; ty = Mark.add Pos.no_pos (TLit TBool) })
           in
           ScopeName.Map.add name

From a58e488532ab6116b55f009367d9521346df03b6 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Mon, 19 Jun 2023 15:30:09 +0200
Subject: [PATCH 05/31] Generate possible values for variables in scope

---
 compiler/verification/conditions.ml | 30 ++++++++++++++++++++++++-----
 compiler/verification/io.ml         | 16 ++++++++++++++-
 2 files changed, 40 insertions(+), 6 deletions(-)

diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index c42fb01dc..283bae314 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -31,6 +31,7 @@ type scope_conditions_ctx = {
   scope_cond_input_vars : typed expr Var.t list;
   scope_cond_variables_typs : (typed expr, typ) Var.Map.t;
   scope_cond_asserts : typed expr list;
+  scope_cond_possible_values : (typed expr, typed expr list) Var.Map.t;
 }
 
 let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) :
@@ -313,6 +314,15 @@ let rec slice_expression_for_date_computations
       (fun e acc -> slice_expression_for_date_computations ctx e @ acc)
       e []
 
+(* Expects a top [EDefault] node and below the tree of defaults. *)
+let rec generate_possible_values (ctx : scope_conditions_ctx) (e : typed expr) :
+    typed expr list =
+  match Mark.remove e with
+  | EDefault { excepts; just = _; cons = c } ->
+    generate_possible_values ctx c
+    @ List.flatten (List.map (generate_possible_values ctx) excepts)
+  | _ -> [e]
+
 (** {1 Interface}*)
 
 type verification_condition_kind =
@@ -327,8 +337,6 @@ type verification_condition = {
   vc_variable : typed expr Var.t Mark.pos;
 }
 
-let trivial_assert e = Mark.copy e (ELit (LBool true))
-
 let rec generate_verification_conditions_scope_body_expr
     (ctx : scope_conditions_ctx)
     (scope_body_expr : 'm expr scope_body_expr) :
@@ -372,6 +380,9 @@ let rec generate_verification_conditions_scope_body_expr
         in
         let e = match_and_ignore_outer_reentrant_default ctx e in
         let vc_confl = generate_vc_must_not_return_conflict ctx e in
+        let possible_values : typed expr list =
+          generate_possible_values ctx e
+        in
         let vc_confl =
           if !Cli.optimize_flag then
             Expr.unbox
@@ -433,7 +444,13 @@ let rec generate_verification_conditions_scope_body_expr
                 })
               subexprs_dates
         in
-        ctx, vc_list
+        ( {
+            ctx with
+            scope_cond_possible_values =
+              Var.Map.add scope_let_var possible_values
+                ctx.scope_cond_possible_values;
+          },
+          vc_list )
       | _ -> ctx, []
     in
     let new_ctx, new_vcs =
@@ -478,7 +495,11 @@ let generate_verification_conditions_code_items
             {
               scope_cond_decls = decl_ctx;
               scope_cond_asserts = [];
+              (* To be filled later *)
               scope_cond_input_vars = [];
+              (* To be filled later *)
+              scope_cond_possible_values = Var.Map.empty;
+              (* To be filled later *)
               scope_cond_variables_typs =
                 Var.Map.empty
                 (* We don't need to add the typ of the scope input var here
@@ -498,8 +519,7 @@ let generate_verification_conditions_code_items
             {
               vc_scope_asserts = combined_assert;
               vc_scope_list = scope_vcs;
-              vc_scope_possible_variable_values =
-                Var.Map.empty (* TODO: implement that!*);
+              vc_scope_possible_variable_values = ctx.scope_cond_possible_values;
             }
             vcs
         else vcs)
diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index 6fbadd28a..2cb2768ab 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -165,13 +165,27 @@ module MakeBackendIO (B : Backend) = struct
       "@[<v>This verification condition was generated for @{<yellow>%s@}:@,\
        %a@,\
        with assertions:@,\
+       %a@,\
+       and possible values for variables:@,\
        %a@]"
       (match vc.vc_kind with
       | Conditions.NoEmptyError ->
         "the variable definition never to return an empty error"
       | NoOverlappingExceptions -> "no two exceptions to ever overlap"
       | DateComputation -> "this date computation cannot be ambiguous")
-      (Print.expr ()) vc.vc_guard (Print.expr ()) vc_scope_ctx.vc_scope_asserts;
+      (Print.expr ()) vc.vc_guard (Print.expr ()) vc_scope_ctx.vc_scope_asserts
+      (fun fmt vars_possible_values ->
+        Format.pp_print_list
+          ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+          (fun fmt (var, values) ->
+            Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
+              (Format.pp_print_list
+                 ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
+                 (Print.expr ()))
+              values)
+          fmt
+          (Var.Map.bindings vars_possible_values))
+      vc_scope_ctx.vc_scope_possible_variable_values;
 
     match z3_vc with
     | Success (encoding, backend_ctx) -> (

From 715422e4f5502814a3a18954360041ad8d4600c5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Wed, 21 Jun 2023 16:07:28 +0200
Subject: [PATCH 06/31] Expression slicing for date comparison (to have more
 interesting results)

---
 compiler/verification/conditions.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 283bae314..e76f55b4c 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -300,7 +300,18 @@ let rec generate_vc_must_not_return_conflict
 let rec slice_expression_for_date_computations
     (ctx : scope_conditions_ctx)
     (e : typed expr) : vc_return list =
+  (* let (Typed { ty = t; _ }) = Mark.get e in  *)
   match Mark.remove e with
+  | EApp
+      {
+        f =
+          EOp { op = Op.Lte_dat_dat | Op.Lt_dat_dat | Op.Gt_dat_dat | Op.Gte_dat_dat; tys = _ }, _;
+        args;
+      } ->
+    let r = List.flatten (List.map (slice_expression_for_date_computations ctx) args) in
+    if r <> [] then
+      [e]
+    else []
   | EApp
       {
         f =

From 1b57934e40b11b82ae034b5b7fd796ad908691b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Wed, 21 Jun 2023 16:08:07 +0200
Subject: [PATCH 07/31] WIP (ugly code) on creating universal programs for date
 ambiguity detection in Mopsa

---
 compiler/shared_ast/var.ml      |   1 +
 compiler/shared_ast/var.mli     |   1 +
 compiler/verification/solver.ml | 159 +++++++++++++++++++++++---------
 3 files changed, 117 insertions(+), 44 deletions(-)

diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index c1760b1a6..bfe637c63 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -76,6 +76,7 @@ module Set = struct
   let of_list l = of_list (List.map t l)
   let elements s = elements s |> List.map get
   let diff s1 s2 = diff s1 s2
+  let choose_opt s = Option.map get (choose_opt s)
 
   (* Add more as needed *)
 end
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index c03e64289..41f0767f6 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -49,6 +49,7 @@ module Set : sig
   val of_list : 'e var list -> 'e t
   val elements : 'e t -> 'e var list
   val diff : 'e t -> 'e t -> 'e t
+  val choose_opt : 'e t -> 'e var option
 end
 
 (** Wrapper over [Map.S] but with a type variable for the AST type parameters.
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index a58e05b68..9c272d610 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -29,50 +29,121 @@ let solve_vcs
   let all_proven =
     ScopeName.Map.fold
       (fun scope_name scope_vcs all_proven ->
-        let dates_vc =
-          List.filter
-            (fun vc ->
-              match vc.Conditions.vc_kind with
-              | Conditions.DateComputation -> true
-              | _ -> false)
-            scope_vcs.Conditions.vc_scope_list
-        in
-        List.iter
-          (fun dates_vc ->
-            Message.emit_result "%s"
-              (Z3backend.Io.print_negative_result dates_vc scope_name
-                 (Z3backend.Io.make_context decl_ctx)
-                 None))
-          dates_vc;
-        let z3_vcs =
-          List.map
-            (fun vc ->
-              ( vc,
-                try
-                  let ctx = Z3backend.Io.make_context decl_ctx in
-                  let ctx =
-                    Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
-                  in
-                  let ctx, z3_vc =
-                    Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
-                  in
-                  Z3backend.Io.Success (z3_vc, ctx)
-                with Failure msg -> Fail msg ))
-            (List.filter
-               (fun vc ->
-                 match vc.Conditions.vc_kind with
-                 | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
-                   ->
-                   true
-                 | Conditions.DateComputation -> false)
-               scope_vcs.Conditions.vc_scope_list)
-        in
-        List.fold_left
-          (fun all_proven vc ->
-            if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
-              all_proven
-            else false)
-          all_proven z3_vcs)
+         let dates_vc =
+           List.filter
+             (fun vc ->
+                match vc.Conditions.vc_kind with
+                | Conditions.DateComputation -> true
+                | _ -> false)
+             scope_vcs.Conditions.vc_scope_list
+         in
+         List.iter
+           (fun dates_vc ->
+              Message.emit_result "%s"
+                (Z3backend.Io.print_negative_result dates_vc scope_name
+                   (Z3backend.Io.make_context decl_ctx)
+                   None);
+              let vc = dates_vc in
+              let vc_scope_ctx = scope_vcs in
+              let interesting_vars =
+                let rec collect_vars = function
+                  | EVar v, _ -> Var.Set.singleton v
+                  | e -> Expr.shallow_fold (fun e -> Var.Set.union (collect_vars e)) e Var.Set.empty in
+                let rec related_vars todos acc =
+                  match Var.Set.choose_opt todos with
+                  | None -> acc
+                  | Some t ->
+                    let new_vars = List.fold_left (fun acc e ->
+                        Var.Set.union acc (collect_vars e))
+                        Var.Set.empty 
+                        (Option.value ~default:[] (Var.Map.find_opt t vc_scope_ctx.vc_scope_possible_variable_values)) in
+                    related_vars (Var.Set.union (Var.Set.remove t todos) new_vars) (Var.Set.union acc new_vars)
+                in
+                related_vars (collect_vars vc.vc_guard)  (collect_vars vc.vc_guard)
+              in
+              Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values: %a@."
+                (Print.expr ()) vc.vc_guard (Print.expr ()) vc_scope_ctx.vc_scope_asserts
+                (fun fmt vars_possible_values ->
+                   Format.pp_print_list
+                     ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+                     (fun fmt (var, values) ->
+                        if Var.Set.mem var interesting_vars then 
+                          Format.fprintf fmt "<IMP>";
+                        Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
+                          (Format.pp_print_list
+                             ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
+                             (fun fmt expr -> Print.expr () fmt expr))
+                          values;
+                        if Var.Set.mem var interesting_vars then 
+                          Format.fprintf fmt "</IMP>";
+                     )
+                     fmt
+                     (* (List.filter (fun (var, values) -> *)
+                     (*    ) *)
+                         (Var.Map.bindings vars_possible_values))
+                vc_scope_ctx.vc_scope_possible_variable_values;
+              let universal_program =
+                (* The goal of this part is to extract additions from expressions, and perform them before as assignments. This will simplify the analysis and communication with Mopsa. We can assume there are no binders to handle  *)
+                let trivial_map_union = (Var.Map.union (fun _ _ _ -> assert false)) in
+                let rec separate_additions e =
+                  match Mark.remove e with
+                  | EApp
+                      {
+                        f =
+                          (EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound; tys = _ }, _) as f;
+                        args;
+                      } ->
+                    let acc, args = List.fold_left_map
+                        (fun acc arg ->
+                           let toadd, arg = separate_additions arg in
+                           trivial_map_union acc toadd, arg)
+                        Var.Map.empty
+                        args in
+                    let dummy_var =
+                      let pos = Expr.pos e in
+                      let basename = Filename.basename (Pos.get_file pos) |> Filename.chop_extension in
+                      Var.make (Format.asprintf "var_%s_%d-%d_%d-%d"basename (Pos.get_start_line pos) (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)) in
+                    let new_e = Expr.unbox (Expr.eapp (Expr.box f) args (Mark.get e)) in
+                    Var.Map.add dummy_var new_e acc,
+                    Expr.evar dummy_var (Mark.get e)
+                  | _ ->
+                    Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union ~f:separate_additions e in
+                let new_vars, simple_guard = separate_additions vc.vc_guard in
+                let prog = Var.Map.fold (fun var expr acc ->
+                    Format.asprintf "%a %a = %a@."  (Print.typ decl_ctx) (Expr.ty expr)  (Print.var) var (Print.expr ()) expr ^ acc) new_vars "" ^ Format.asprintf "assert(sync(%a))" (Print.expr ()) (Expr.unbox simple_guard) in
+                Format.eprintf "Prog:@.%s@." prog
+              in ()
+           )
+           dates_vc;
+         let z3_vcs =
+           List.map
+             (fun vc ->
+                ( vc,
+                  try
+                    let ctx = Z3backend.Io.make_context decl_ctx in
+                    let ctx =
+                      Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
+                    in
+                    let ctx, z3_vc =
+                      Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
+                    in
+                    Z3backend.Io.Success (z3_vc, ctx)
+                  with Failure msg -> Fail msg ))
+             (List.filter
+                (fun vc ->
+                   match vc.Conditions.vc_kind with
+                   | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
+                     ->
+                     true
+                   | Conditions.DateComputation -> false)
+                scope_vcs.Conditions.vc_scope_list)
+         in
+         List.fold_left
+           (fun all_proven vc ->
+              if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
+                all_proven
+              else false)
+           all_proven z3_vcs)
       vcs true
   in
   if all_proven then

From e57fb0436df239039d9575e88a7f9f1e5492e705 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Thu, 22 Jun 2023 13:22:54 +0200
Subject: [PATCH 08/31] Formatting

---
 compiler/verification/conditions.ml |  19 +-
 compiler/verification/solver.ml     | 266 ++++++++++++++++------------
 2 files changed, 166 insertions(+), 119 deletions(-)

diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index e76f55b4c..087777cff 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -300,18 +300,25 @@ let rec generate_vc_must_not_return_conflict
 let rec slice_expression_for_date_computations
     (ctx : scope_conditions_ctx)
     (e : typed expr) : vc_return list =
-  (* let (Typed { ty = t; _ }) = Mark.get e in  *)
+  (* let (Typed { ty = t; _ }) = Mark.get e in *)
   match Mark.remove e with
   | EApp
       {
         f =
-          EOp { op = Op.Lte_dat_dat | Op.Lt_dat_dat | Op.Gt_dat_dat | Op.Gte_dat_dat; tys = _ }, _;
+          ( EOp
+              {
+                op =
+                  ( Op.Lte_dat_dat | Op.Lt_dat_dat | Op.Gt_dat_dat
+                  | Op.Gte_dat_dat );
+                tys = _;
+              },
+            _ );
         args;
       } ->
-    let r = List.flatten (List.map (slice_expression_for_date_computations ctx) args) in
-    if r <> [] then
-      [e]
-    else []
+    let r =
+      List.flatten (List.map (slice_expression_for_date_computations ctx) args)
+    in
+    if r <> [] then [e] else []
   | EApp
       {
         f =
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 9c272d610..3e2b0ea60 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -29,121 +29,161 @@ let solve_vcs
   let all_proven =
     ScopeName.Map.fold
       (fun scope_name scope_vcs all_proven ->
-         let dates_vc =
-           List.filter
-             (fun vc ->
-                match vc.Conditions.vc_kind with
-                | Conditions.DateComputation -> true
-                | _ -> false)
-             scope_vcs.Conditions.vc_scope_list
-         in
-         List.iter
-           (fun dates_vc ->
-              Message.emit_result "%s"
-                (Z3backend.Io.print_negative_result dates_vc scope_name
-                   (Z3backend.Io.make_context decl_ctx)
-                   None);
-              let vc = dates_vc in
-              let vc_scope_ctx = scope_vcs in
-              let interesting_vars =
-                let rec collect_vars = function
-                  | EVar v, _ -> Var.Set.singleton v
-                  | e -> Expr.shallow_fold (fun e -> Var.Set.union (collect_vars e)) e Var.Set.empty in
-                let rec related_vars todos acc =
-                  match Var.Set.choose_opt todos with
-                  | None -> acc
-                  | Some t ->
-                    let new_vars = List.fold_left (fun acc e ->
-                        Var.Set.union acc (collect_vars e))
-                        Var.Set.empty 
-                        (Option.value ~default:[] (Var.Map.find_opt t vc_scope_ctx.vc_scope_possible_variable_values)) in
-                    related_vars (Var.Set.union (Var.Set.remove t todos) new_vars) (Var.Set.union acc new_vars)
-                in
-                related_vars (collect_vars vc.vc_guard)  (collect_vars vc.vc_guard)
+        let dates_vc =
+          List.filter
+            (fun vc ->
+              match vc.Conditions.vc_kind with
+              | Conditions.DateComputation -> true
+              | _ -> false)
+            scope_vcs.Conditions.vc_scope_list
+        in
+        List.iter
+          (fun dates_vc ->
+            Message.emit_result "%s"
+              (Z3backend.Io.print_negative_result dates_vc scope_name
+                 (Z3backend.Io.make_context decl_ctx)
+                 None);
+            let vc = dates_vc in
+            let vc_scope_ctx = scope_vcs in
+            let interesting_vars =
+              let rec collect_vars = function
+                | EVar v, _ -> Var.Set.singleton v
+                | e ->
+                  Expr.shallow_fold
+                    (fun e -> Var.Set.union (collect_vars e))
+                    e Var.Set.empty
               in
-              Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values: %a@."
-                (Print.expr ()) vc.vc_guard (Print.expr ()) vc_scope_ctx.vc_scope_asserts
-                (fun fmt vars_possible_values ->
-                   Format.pp_print_list
-                     ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
-                     (fun fmt (var, values) ->
-                        if Var.Set.mem var interesting_vars then 
-                          Format.fprintf fmt "<IMP>";
-                        Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
-                          (Format.pp_print_list
-                             ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
-                             (fun fmt expr -> Print.expr () fmt expr))
-                          values;
-                        if Var.Set.mem var interesting_vars then 
-                          Format.fprintf fmt "</IMP>";
-                     )
-                     fmt
-                     (* (List.filter (fun (var, values) -> *)
-                     (*    ) *)
-                         (Var.Map.bindings vars_possible_values))
-                vc_scope_ctx.vc_scope_possible_variable_values;
-              let universal_program =
-                (* The goal of this part is to extract additions from expressions, and perform them before as assignments. This will simplify the analysis and communication with Mopsa. We can assume there are no binders to handle  *)
-                let trivial_map_union = (Var.Map.union (fun _ _ _ -> assert false)) in
-                let rec separate_additions e =
-                  match Mark.remove e with
-                  | EApp
-                      {
-                        f =
-                          (EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound; tys = _ }, _) as f;
-                        args;
-                      } ->
-                    let acc, args = List.fold_left_map
-                        (fun acc arg ->
-                           let toadd, arg = separate_additions arg in
-                           trivial_map_union acc toadd, arg)
-                        Var.Map.empty
-                        args in
-                    let dummy_var =
-                      let pos = Expr.pos e in
-                      let basename = Filename.basename (Pos.get_file pos) |> Filename.chop_extension in
-                      Var.make (Format.asprintf "var_%s_%d-%d_%d-%d"basename (Pos.get_start_line pos) (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)) in
-                    let new_e = Expr.unbox (Expr.eapp (Expr.box f) args (Mark.get e)) in
-                    Var.Map.add dummy_var new_e acc,
-                    Expr.evar dummy_var (Mark.get e)
-                  | _ ->
-                    Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union ~f:separate_additions e in
-                let new_vars, simple_guard = separate_additions vc.vc_guard in
-                let prog = Var.Map.fold (fun var expr acc ->
-                    Format.asprintf "%a %a = %a@."  (Print.typ decl_ctx) (Expr.ty expr)  (Print.var) var (Print.expr ()) expr ^ acc) new_vars "" ^ Format.asprintf "assert(sync(%a))" (Print.expr ()) (Expr.unbox simple_guard) in
-                Format.eprintf "Prog:@.%s@." prog
-              in ()
-           )
-           dates_vc;
-         let z3_vcs =
-           List.map
-             (fun vc ->
-                ( vc,
-                  try
-                    let ctx = Z3backend.Io.make_context decl_ctx in
-                    let ctx =
-                      Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
-                    in
-                    let ctx, z3_vc =
-                      Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
+              let rec related_vars todos acc =
+                match Var.Set.choose_opt todos with
+                | None -> acc
+                | Some t ->
+                  let new_vars =
+                    List.fold_left
+                      (fun acc e -> Var.Set.union acc (collect_vars e))
+                      Var.Set.empty
+                      (Option.value ~default:[]
+                         (Var.Map.find_opt t
+                            vc_scope_ctx.vc_scope_possible_variable_values))
+                  in
+                  related_vars
+                    (Var.Set.union (Var.Set.remove t todos) new_vars)
+                    (Var.Set.union acc new_vars)
+              in
+              related_vars (collect_vars vc.vc_guard) (collect_vars vc.vc_guard)
+            in
+            Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values: %a@."
+              (Print.expr ()) vc.vc_guard (Print.expr ())
+              vc_scope_ctx.vc_scope_asserts
+              (fun fmt vars_possible_values ->
+                Format.pp_print_list
+                  ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+                  (fun fmt (var, values) ->
+                    if Var.Set.mem var interesting_vars then
+                      Format.fprintf fmt "<IMP>";
+                    Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
+                      (Format.pp_print_list
+                         ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
+                         (fun fmt expr -> Print.expr () fmt expr))
+                      values;
+                    if Var.Set.mem var interesting_vars then
+                      Format.fprintf fmt "</IMP>")
+                  fmt
+                  (* (List.filter (fun (var, values) -> *)
+                  (*    ) *)
+                  (Var.Map.bindings vars_possible_values))
+              vc_scope_ctx.vc_scope_possible_variable_values;
+            let universal_program =
+              (* The goal of this part is to extract additions from expressions,
+                 and perform them before as assignments. This will simplify the
+                 analysis and communication with Mopsa. We can assume there are
+                 no binders to handle *)
+              let trivial_map_union =
+                Var.Map.union (fun _ _ _ -> assert false)
+              in
+              let rec separate_additions e =
+                match Mark.remove e with
+                | EApp
+                    {
+                      f =
+                        ( EOp
+                            {
+                              op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound;
+                              tys = _;
+                            },
+                          _ ) as f;
+                      args;
+                    } ->
+                  let acc, args =
+                    List.fold_left_map
+                      (fun acc arg ->
+                        let toadd, arg = separate_additions arg in
+                        trivial_map_union acc toadd, arg)
+                      Var.Map.empty args
+                  in
+                  let dummy_var =
+                    let pos = Expr.pos e in
+                    let basename =
+                      Filename.basename (Pos.get_file pos)
+                      |> Filename.chop_extension
                     in
-                    Z3backend.Io.Success (z3_vc, ctx)
-                  with Failure msg -> Fail msg ))
-             (List.filter
-                (fun vc ->
-                   match vc.Conditions.vc_kind with
-                   | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
-                     ->
-                     true
-                   | Conditions.DateComputation -> false)
-                scope_vcs.Conditions.vc_scope_list)
-         in
-         List.fold_left
-           (fun all_proven vc ->
-              if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
-                all_proven
-              else false)
-           all_proven z3_vcs)
+                    Var.make
+                      (Format.asprintf "var_%s_%d-%d_%d-%d" basename
+                         (Pos.get_start_line pos) (Pos.get_start_column pos)
+                         (Pos.get_end_line pos) (Pos.get_end_column pos))
+                  in
+                  let new_e =
+                    Expr.unbox (Expr.eapp (Expr.box f) args (Mark.get e))
+                  in
+                  ( Var.Map.add dummy_var new_e acc,
+                    Expr.evar dummy_var (Mark.get e) )
+                | _ ->
+                  Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union
+                    ~f:separate_additions e
+              in
+              let new_vars, simple_guard = separate_additions vc.vc_guard in
+              let prog =
+                Var.Map.fold
+                  (fun var expr acc ->
+                    Format.asprintf "%a %a = %a@." (Print.typ decl_ctx)
+                      (Expr.ty expr) Print.var var (Print.expr ()) expr
+                    ^ acc)
+                  new_vars ""
+                ^ Format.asprintf "assert(sync(%a))" (Print.expr ())
+                    (Expr.unbox simple_guard)
+              in
+              Format.eprintf "Prog:@.%s@." prog
+            in
+            ())
+          dates_vc;
+        let z3_vcs =
+          List.map
+            (fun vc ->
+              ( vc,
+                try
+                  let ctx = Z3backend.Io.make_context decl_ctx in
+                  let ctx =
+                    Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
+                  in
+                  let ctx, z3_vc =
+                    Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
+                  in
+                  Z3backend.Io.Success (z3_vc, ctx)
+                with Failure msg -> Fail msg ))
+            (List.filter
+               (fun vc ->
+                 match vc.Conditions.vc_kind with
+                 | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
+                   ->
+                   true
+                 | Conditions.DateComputation -> false)
+               scope_vcs.Conditions.vc_scope_list)
+        in
+        List.fold_left
+          (fun all_proven vc ->
+            if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
+              all_proven
+            else false)
+          all_proven z3_vcs)
       vcs true
   in
   if all_proven then

From fcc19f1a871c63379bf911fe3ce5fa301fda276c Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Thu, 22 Jun 2023 14:11:15 +0200
Subject: [PATCH 09/31] Refactor code and solve bindling problems

---
 compiler/shared_ast/var.ml      |   1 +
 compiler/shared_ast/var.mli     |   1 +
 compiler/verification/solver.ml | 253 +++++++++++++++++---------------
 3 files changed, 137 insertions(+), 118 deletions(-)

diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index bfe637c63..ccddbf35d 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -96,6 +96,7 @@ module Map = struct
   let find v m = find (t v) m
   let find_opt v m = find_opt (t v) m
   let bindings m = bindings m |> List.map (fun (v, x) -> get v, x)
+  let map f m = map f m
   let mem x m = mem (t x) m
   let union f m1 m2 = union (fun v x1 x2 -> f (get v) x1 x2) m1 m2
   let fold f m acc = fold (fun v x acc -> f (get v) x acc) m acc
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index 41f0767f6..5f06e1cc2 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -65,6 +65,7 @@ module Map : sig
   val find_opt : 'e var -> ('e, 'x) t -> 'x option
   val bindings : ('e, 'x) t -> ('e var * 'x) list
   val mem : 'e var -> ('e, 'x) t -> bool
+  val map : ('x -> 'y) -> ('e, 'x) t -> ('e, 'y) t
 
   val union :
     ('e var -> 'x -> 'x -> 'x option) -> ('e, 'x) t -> ('e, 'x) t -> ('e, 'x) t
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 3e2b0ea60..c59608034 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -17,6 +17,140 @@
 open Catala_utils
 open Shared_ast
 
+module TypedValuesDcalcVarMap = struct
+  type 'x t = (typed Dcalc.Ast.expr, ('x, typed) marked) Var.Map.t
+
+  let map (f : 'a -> 'b) (m : 'a t) : 'b t =
+    Var.Map.map (fun (x, tx) -> f x, tx) m
+end
+
+module TypedValuesDcalcVarMapBoxLifting = Bindlib.Lift (TypedValuesDcalcVarMap)
+
+type mopsa_program = {
+  main_guard : typed Dcalc.Ast.expr;
+  other_values : (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr) Var.Map.t;
+}
+
+(* The goal of this part is to extract additions from expressions, and perform
+   them before as assignments. This will simplify the analysis and communication
+   with Mopsa. *)
+let turn_vc_into_mopsa_compatible_program
+    (vc : Conditions.verification_condition) : mopsa_program =
+  let trivial_map_union = Var.Map.union (fun _ _ _ -> assert false) in
+  let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
+      (typed Dcalc.Ast.expr, (dcalc, typed) boxed_gexpr) Var.Map.t
+      * (dcalc, typed) boxed_gexpr =
+    match Mark.remove e with
+    | EApp
+        {
+          f =
+            ( EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound; tys = _ },
+              _ ) as f;
+          args;
+        } ->
+      let acc, args =
+        List.fold_left_map
+          (fun acc arg ->
+            let toadd, arg = split_expression_into_atomic_parts arg in
+            trivial_map_union acc toadd, arg)
+          Var.Map.empty args
+      in
+      let dummy_var =
+        let pos = Expr.pos e in
+        let basename =
+          Filename.basename (Pos.get_file pos) |> Filename.chop_extension
+        in
+        Var.make
+          (Format.asprintf "var_%s_%d-%d_%d-%d" basename
+             (Pos.get_start_line pos) (Pos.get_start_column pos)
+             (Pos.get_end_line pos) (Pos.get_end_column pos))
+      in
+      let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
+      Var.Map.add dummy_var new_e acc, Expr.evar dummy_var (Mark.get e)
+    | _ ->
+      Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union
+        ~f:split_expression_into_atomic_parts e
+  in
+  let new_vars, (simple_guard, simple_guard_mark) =
+    split_expression_into_atomic_parts vc.vc_guard
+  in
+  let new_vars, simple_guard =
+    (* This manipulation is done so that we only unbox once to keep all
+       variables in sync. *)
+    Bindlib.unbox
+      (Bindlib.box_apply2
+         (fun new_vars simple_guard ->
+           new_vars, (simple_guard, simple_guard_mark))
+         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars)
+         simple_guard)
+  in
+  { main_guard = simple_guard; other_values = new_vars }
+
+(** This function is temporarily here but should be moved to a MOPSA backend. *)
+let solve_date_vc
+    (decl_ctx : decl_ctx)
+    (scope_name : ScopeName.t)
+    (vc_scope_ctx : Conditions.verification_conditions_scope)
+    (vc : Conditions.verification_condition) =
+  Message.emit_debug "%s"
+    (Z3backend.Io.print_negative_result vc scope_name
+       (Z3backend.Io.make_context decl_ctx)
+       None);
+  let interesting_vars =
+    let rec collect_vars = function
+      | EVar v, _ -> Var.Set.singleton v
+      | e ->
+        Expr.shallow_fold
+          (fun e -> Var.Set.union (collect_vars e))
+          e Var.Set.empty
+    in
+    let rec related_vars todos acc =
+      match Var.Set.choose_opt todos with
+      | None -> acc
+      | Some t ->
+        let new_vars =
+          List.fold_left
+            (fun acc e -> Var.Set.union acc (collect_vars e))
+            Var.Set.empty
+            (Option.value ~default:[]
+               (Var.Map.find_opt t
+                  vc_scope_ctx.Conditions.vc_scope_possible_variable_values))
+        in
+        related_vars
+          (Var.Set.union (Var.Set.remove t todos) new_vars)
+          (Var.Set.union acc new_vars)
+    in
+    related_vars (collect_vars vc.vc_guard) (collect_vars vc.vc_guard)
+  in
+  Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values: %a@."
+    (Print.expr ()) vc.vc_guard (Print.expr ())
+    vc_scope_ctx.Conditions.vc_scope_asserts
+    (fun fmt vars_possible_values ->
+      Format.pp_print_list
+        ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+        (fun fmt (var, values) ->
+          if Var.Set.mem var interesting_vars then Format.fprintf fmt "<IMP>";
+          Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
+            (Format.pp_print_list
+               ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
+               (fun fmt expr -> Print.expr () fmt expr))
+            values;
+          if Var.Set.mem var interesting_vars then Format.fprintf fmt "</IMP>")
+        fmt
+        (Var.Map.bindings vars_possible_values))
+    vc_scope_ctx.Conditions.vc_scope_possible_variable_values;
+  let prog = turn_vc_into_mopsa_compatible_program vc in
+  let prog_string =
+    Var.Map.fold
+      (fun var expr acc ->
+        Format.asprintf "%a %a = %a@." (Print.typ decl_ctx) (Expr.ty expr)
+          Print.var_debug var (Print.expr ()) expr
+        ^ acc)
+      prog.other_values ""
+    ^ Format.asprintf "assert(sync(%a))" (Print.expr ()) prog.main_guard
+  in
+  Format.eprintf "Prog:@.%s@." prog_string
+
 (** [solve_vc] is the main entry point of this module. It takes a list of
     expressions [vcs] corresponding to verification conditions that must be
     discharged by Z3, and attempts to solve them **)
@@ -37,124 +171,7 @@ let solve_vcs
               | _ -> false)
             scope_vcs.Conditions.vc_scope_list
         in
-        List.iter
-          (fun dates_vc ->
-            Message.emit_result "%s"
-              (Z3backend.Io.print_negative_result dates_vc scope_name
-                 (Z3backend.Io.make_context decl_ctx)
-                 None);
-            let vc = dates_vc in
-            let vc_scope_ctx = scope_vcs in
-            let interesting_vars =
-              let rec collect_vars = function
-                | EVar v, _ -> Var.Set.singleton v
-                | e ->
-                  Expr.shallow_fold
-                    (fun e -> Var.Set.union (collect_vars e))
-                    e Var.Set.empty
-              in
-              let rec related_vars todos acc =
-                match Var.Set.choose_opt todos with
-                | None -> acc
-                | Some t ->
-                  let new_vars =
-                    List.fold_left
-                      (fun acc e -> Var.Set.union acc (collect_vars e))
-                      Var.Set.empty
-                      (Option.value ~default:[]
-                         (Var.Map.find_opt t
-                            vc_scope_ctx.vc_scope_possible_variable_values))
-                  in
-                  related_vars
-                    (Var.Set.union (Var.Set.remove t todos) new_vars)
-                    (Var.Set.union acc new_vars)
-              in
-              related_vars (collect_vars vc.vc_guard) (collect_vars vc.vc_guard)
-            in
-            Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values: %a@."
-              (Print.expr ()) vc.vc_guard (Print.expr ())
-              vc_scope_ctx.vc_scope_asserts
-              (fun fmt vars_possible_values ->
-                Format.pp_print_list
-                  ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
-                  (fun fmt (var, values) ->
-                    if Var.Set.mem var interesting_vars then
-                      Format.fprintf fmt "<IMP>";
-                    Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
-                      (Format.pp_print_list
-                         ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
-                         (fun fmt expr -> Print.expr () fmt expr))
-                      values;
-                    if Var.Set.mem var interesting_vars then
-                      Format.fprintf fmt "</IMP>")
-                  fmt
-                  (* (List.filter (fun (var, values) -> *)
-                  (*    ) *)
-                  (Var.Map.bindings vars_possible_values))
-              vc_scope_ctx.vc_scope_possible_variable_values;
-            let universal_program =
-              (* The goal of this part is to extract additions from expressions,
-                 and perform them before as assignments. This will simplify the
-                 analysis and communication with Mopsa. We can assume there are
-                 no binders to handle *)
-              let trivial_map_union =
-                Var.Map.union (fun _ _ _ -> assert false)
-              in
-              let rec separate_additions e =
-                match Mark.remove e with
-                | EApp
-                    {
-                      f =
-                        ( EOp
-                            {
-                              op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound;
-                              tys = _;
-                            },
-                          _ ) as f;
-                      args;
-                    } ->
-                  let acc, args =
-                    List.fold_left_map
-                      (fun acc arg ->
-                        let toadd, arg = separate_additions arg in
-                        trivial_map_union acc toadd, arg)
-                      Var.Map.empty args
-                  in
-                  let dummy_var =
-                    let pos = Expr.pos e in
-                    let basename =
-                      Filename.basename (Pos.get_file pos)
-                      |> Filename.chop_extension
-                    in
-                    Var.make
-                      (Format.asprintf "var_%s_%d-%d_%d-%d" basename
-                         (Pos.get_start_line pos) (Pos.get_start_column pos)
-                         (Pos.get_end_line pos) (Pos.get_end_column pos))
-                  in
-                  let new_e =
-                    Expr.unbox (Expr.eapp (Expr.box f) args (Mark.get e))
-                  in
-                  ( Var.Map.add dummy_var new_e acc,
-                    Expr.evar dummy_var (Mark.get e) )
-                | _ ->
-                  Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union
-                    ~f:separate_additions e
-              in
-              let new_vars, simple_guard = separate_additions vc.vc_guard in
-              let prog =
-                Var.Map.fold
-                  (fun var expr acc ->
-                    Format.asprintf "%a %a = %a@." (Print.typ decl_ctx)
-                      (Expr.ty expr) Print.var var (Print.expr ()) expr
-                    ^ acc)
-                  new_vars ""
-                ^ Format.asprintf "assert(sync(%a))" (Print.expr ())
-                    (Expr.unbox simple_guard)
-              in
-              Format.eprintf "Prog:@.%s@." prog
-            in
-            ())
-          dates_vc;
+        List.iter (solve_date_vc decl_ctx scope_name scope_vcs) dates_vc;
         let z3_vcs =
           List.map
             (fun vc ->

From 174047326af5e6d11214f7ab3478eeabbe4afdcc Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Thu, 22 Jun 2023 14:33:32 +0200
Subject: [PATCH 10/31] Simplify code

---
 compiler/shared_ast/var.ml      |  1 +
 compiler/shared_ast/var.mli     |  1 +
 compiler/verification/solver.ml | 48 +++++++++++----------------------
 3 files changed, 17 insertions(+), 33 deletions(-)

diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index ccddbf35d..3d21527f2 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -77,6 +77,7 @@ module Set = struct
   let elements s = elements s |> List.map get
   let diff s1 s2 = diff s1 s2
   let choose_opt s = Option.map get (choose_opt s)
+  let filter f s = filter (fun v -> f (get v)) s
 
   (* Add more as needed *)
 end
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index 5f06e1cc2..39241f6ef 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -50,6 +50,7 @@ module Set : sig
   val elements : 'e t -> 'e var list
   val diff : 'e t -> 'e t -> 'e t
   val choose_opt : 'e t -> 'e var option
+  val filter : ('e var -> bool) -> 'e t -> 'e t
 end
 
 (** Wrapper over [Map.S] but with a type variable for the AST type parameters.
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index c59608034..8babdf36b 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -96,46 +96,28 @@ let solve_date_vc
     (Z3backend.Io.print_negative_result vc scope_name
        (Z3backend.Io.make_context decl_ctx)
        None);
-  let interesting_vars =
-    let rec collect_vars = function
-      | EVar v, _ -> Var.Set.singleton v
-      | e ->
-        Expr.shallow_fold
-          (fun e -> Var.Set.union (collect_vars e))
-          e Var.Set.empty
-    in
-    let rec related_vars todos acc =
-      match Var.Set.choose_opt todos with
-      | None -> acc
-      | Some t ->
-        let new_vars =
-          List.fold_left
-            (fun acc e -> Var.Set.union acc (collect_vars e))
-            Var.Set.empty
-            (Option.value ~default:[]
-               (Var.Map.find_opt t
-                  vc_scope_ctx.Conditions.vc_scope_possible_variable_values))
-        in
-        related_vars
-          (Var.Set.union (Var.Set.remove t todos) new_vars)
-          (Var.Set.union acc new_vars)
-    in
-    related_vars (collect_vars vc.vc_guard) (collect_vars vc.vc_guard)
+  let vars_used_in_vc = Expr.free_vars vc.vc_guard in
+  let vars_used_in_vc_with_known_values =
+    Var.Set.filter
+      (fun v ->
+        Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
+      vars_used_in_vc
   in
-  Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values: %a@."
+  Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values:@.%a@."
     (Print.expr ()) vc.vc_guard (Print.expr ())
     vc_scope_ctx.Conditions.vc_scope_asserts
     (fun fmt vars_possible_values ->
       Format.pp_print_list
         ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
         (fun fmt (var, values) ->
-          if Var.Set.mem var interesting_vars then Format.fprintf fmt "<IMP>";
-          Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
-            (Format.pp_print_list
-               ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
-               (fun fmt expr -> Print.expr () fmt expr))
-            values;
-          if Var.Set.mem var interesting_vars then Format.fprintf fmt "</IMP>")
+          if Var.Set.mem var vars_used_in_vc_with_known_values then (
+            Format.fprintf fmt "<IMP>";
+            Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var_debug var
+              (Format.pp_print_list
+                 ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
+                 (fun fmt expr -> Print.expr () fmt expr))
+              values;
+            Format.fprintf fmt "</IMP>"))
         fmt
         (Var.Map.bindings vars_possible_values))
     vc_scope_ctx.Conditions.vc_scope_possible_variable_values;

From 7d4d3e8ccc8baed5c09b8743621a794d655b7d5d Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Thu, 22 Jun 2023 14:48:51 +0200
Subject: [PATCH 11/31] Identify unknown variables

---
 compiler/shared_ast/var.ml           |  1 +
 compiler/shared_ast/var.mli          |  1 +
 compiler/verification/conditions.ml  | 32 +++++++++++++++++++---------
 compiler/verification/conditions.mli |  1 +
 compiler/verification/solver.ml      | 24 ++++++++++++++++++---
 5 files changed, 46 insertions(+), 13 deletions(-)

diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index 3d21527f2..b07af1141 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -78,6 +78,7 @@ module Set = struct
   let diff s1 s2 = diff s1 s2
   let choose_opt s = Option.map get (choose_opt s)
   let filter f s = filter (fun v -> f (get v)) s
+  let exists f s = exists (fun v -> f (get v)) s
 
   (* Add more as needed *)
 end
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index 39241f6ef..15eb7c524 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -51,6 +51,7 @@ module Set : sig
   val diff : 'e t -> 'e t -> 'e t
   val choose_opt : 'e t -> 'e var option
   val filter : ('e var -> bool) -> 'e t -> 'e t
+  val exists : ('e var -> bool) -> 'e t -> bool
 end
 
 (** Wrapper over [Map.S] but with a type variable for the AST type parameters.
diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 087777cff..ec00faa76 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -28,7 +28,8 @@ type vc_return = typed expr
 
 type scope_conditions_ctx = {
   scope_cond_decls : decl_ctx;
-  scope_cond_input_vars : typed expr Var.t list;
+  scope_cond_input_vars : typed expr Var.Set.t;
+  scope_cond_subscope_output_vars : typed expr Var.Set.t;
   scope_cond_variables_typs : (typed expr, typ) Var.Map.t;
   scope_cond_asserts : typed expr list;
   scope_cond_possible_values : (typed expr, typed expr list) Var.Map.t;
@@ -124,7 +125,7 @@ let match_and_ignore_outer_reentrant_default
             cons;
           },
         _ )
-    when List.exists (fun x' -> Var.eq x x') ctx.scope_cond_input_vars ->
+    when Var.Set.exists (fun x' -> Var.eq x x') ctx.scope_cond_input_vars ->
     (* scope variables*)
     cons
   | EAbs { binder; tys = [(TLit TUnit, _)] } ->
@@ -384,7 +385,15 @@ let rec generate_verification_conditions_scope_body_expr
       | DestructuringInputStruct ->
         ( {
             ctx with
-            scope_cond_input_vars = scope_let_var :: ctx.scope_cond_input_vars;
+            scope_cond_input_vars =
+              Var.Set.add scope_let_var ctx.scope_cond_input_vars;
+          },
+          [] )
+      | DestructuringSubScopeResults ->
+        ( {
+            ctx with
+            scope_cond_input_vars =
+              Var.Set.add scope_let_var ctx.scope_cond_subscope_output_vars;
           },
           [] )
       | ScopeVarDefinition | SubScopeVarDefinition ->
@@ -469,7 +478,7 @@ let rec generate_verification_conditions_scope_body_expr
                 ctx.scope_cond_possible_values;
           },
           vc_list )
-      | _ -> ctx, []
+      | CallingSubScope -> ctx, []
     in
     let new_ctx, new_vcs =
       generate_verification_conditions_scope_body_expr
@@ -487,6 +496,7 @@ type verification_conditions_scope = {
   vc_scope_asserts : typed expr;
   vc_scope_possible_variable_values :
     (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
+  vc_scope_variables_defined_outside_of_scope : typed Dcalc.Ast.expr Var.Set.t;
   vc_scope_list : verification_condition list;
 }
 
@@ -509,15 +519,13 @@ let generate_verification_conditions_code_items
           let _scope_input_var, scope_body_expr =
             Bindlib.unbind body.scope_body_expr
           in
-          let ctx =
+          let init_ctx =
             {
               scope_cond_decls = decl_ctx;
               scope_cond_asserts = [];
-              (* To be filled later *)
-              scope_cond_input_vars = [];
-              (* To be filled later *)
+              scope_cond_input_vars = Var.Set.empty;
               scope_cond_possible_values = Var.Map.empty;
-              (* To be filled later *)
+              scope_cond_subscope_output_vars = Var.Set.empty;
               scope_cond_variables_typs =
                 Var.Map.empty
                 (* We don't need to add the typ of the scope input var here
@@ -527,7 +535,8 @@ let generate_verification_conditions_code_items
             }
           in
           let ctx, scope_vcs =
-            generate_verification_conditions_scope_body_expr ctx scope_body_expr
+            generate_verification_conditions_scope_body_expr init_ctx
+              scope_body_expr
           in
           let combined_assert =
             conjunction_exprs ctx.scope_cond_asserts
@@ -538,6 +547,9 @@ let generate_verification_conditions_code_items
               vc_scope_asserts = combined_assert;
               vc_scope_list = scope_vcs;
               vc_scope_possible_variable_values = ctx.scope_cond_possible_values;
+              vc_scope_variables_defined_outside_of_scope =
+                Var.Set.union ctx.scope_cond_input_vars
+                  ctx.scope_cond_subscope_output_vars;
             }
             vcs
         else vcs)
diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli
index 1525c413d..b67b354e5 100644
--- a/compiler/verification/conditions.mli
+++ b/compiler/verification/conditions.mli
@@ -47,6 +47,7 @@ type verification_conditions_scope = {
       (** For each variable, a list containing all the possible values that this
           variable can have. This is a conservative analysis based on the
           traversal of the default tree. *)
+  vc_scope_variables_defined_outside_of_scope : typed Dcalc.Ast.expr Var.Set.t;
   vc_scope_list : verification_condition list;
 }
 
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 8babdf36b..70976605e 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -103,7 +103,14 @@ let solve_date_vc
         Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
       vars_used_in_vc
   in
-  Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values:@.%a@."
+  let vars_used_in_vc_defined_outside_of_scope =
+    Var.Set.filter
+      (fun v ->
+        Var.Set.mem v
+          vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope)
+      vars_used_in_vc
+  in
+  Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values:@.%a@.%a"
     (Print.expr ()) vc.vc_guard (Print.expr ())
     vc_scope_ctx.Conditions.vc_scope_asserts
     (fun fmt vars_possible_values ->
@@ -112,7 +119,7 @@ let solve_date_vc
         (fun fmt (var, values) ->
           if Var.Set.mem var vars_used_in_vc_with_known_values then (
             Format.fprintf fmt "<IMP>";
-            Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var_debug var
+            Format.fprintf fmt "@[<hov 2>%a@ =@ %a@]" Print.var_debug var
               (Format.pp_print_list
                  ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
                  (fun fmt expr -> Print.expr () fmt expr))
@@ -120,7 +127,18 @@ let solve_date_vc
             Format.fprintf fmt "</IMP>"))
         fmt
         (Var.Map.bindings vars_possible_values))
-    vc_scope_ctx.Conditions.vc_scope_possible_variable_values;
+    vc_scope_ctx.Conditions.vc_scope_possible_variable_values
+    (fun fmt variables_defined_out_of_scope ->
+      Format.pp_print_list
+        ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+        (fun fmt var ->
+          if Var.Set.mem var vars_used_in_vc_defined_outside_of_scope then (
+            Format.fprintf fmt "<UNK>";
+            Format.fprintf fmt "@[<hov 2>%a@ =@ unknown@]" Print.var_debug var;
+            Format.fprintf fmt "</UNK>"))
+        fmt
+        (Var.Set.elements variables_defined_out_of_scope))
+    vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope;
   let prog = turn_vc_into_mopsa_compatible_program vc in
   let prog_string =
     Var.Map.fold

From eb10cccb853c605cac184682fc8260fae2ccbdc3 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Fri, 23 Jun 2023 10:15:53 +0200
Subject: [PATCH 12/31] Fix variable categorization and make it recursive

---
 compiler/shared_ast/var.ml          |  1 +
 compiler/shared_ast/var.mli         |  1 +
 compiler/verification/conditions.ml |  2 +-
 compiler/verification/solver.ml     | 45 +++++++++++++++++++++++++----
 4 files changed, 43 insertions(+), 6 deletions(-)

diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index b07af1141..5eeafe189 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -102,6 +102,7 @@ module Map = struct
   let mem x m = mem (t x) m
   let union f m1 m2 = union (fun v x1 x2 -> f (get v) x1 x2) m1 m2
   let fold f m acc = fold (fun v x acc -> f (get v) x acc) m acc
+  let filter f m = filter (fun k v -> f (get k) v) m
 
   (* Add more as needed *)
 end
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index 15eb7c524..9bbb27edf 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -68,6 +68,7 @@ module Map : sig
   val bindings : ('e, 'x) t -> ('e var * 'x) list
   val mem : 'e var -> ('e, 'x) t -> bool
   val map : ('x -> 'y) -> ('e, 'x) t -> ('e, 'y) t
+  val filter : ('e var -> 'x -> bool) -> ('e, 'x) t -> ('e, 'x) t
 
   val union :
     ('e var -> 'x -> 'x -> 'x option) -> ('e, 'x) t -> ('e, 'x) t -> ('e, 'x) t
diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index ec00faa76..03a2fb9c1 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -392,7 +392,7 @@ let rec generate_verification_conditions_scope_body_expr
       | DestructuringSubScopeResults ->
         ( {
             ctx with
-            scope_cond_input_vars =
+            scope_cond_subscope_output_vars =
               Var.Set.add scope_let_var ctx.scope_cond_subscope_output_vars;
           },
           [] )
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 70976605e..095269535 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -96,7 +96,25 @@ let solve_date_vc
     (Z3backend.Io.print_negative_result vc scope_name
        (Z3backend.Io.make_context decl_ctx)
        None);
-  let vars_used_in_vc = Expr.free_vars vc.vc_guard in
+  let rec vars_used_in_vc (e : typed Dcalc.Ast.expr) :
+      typed Dcalc.Ast.expr Var.Set.t =
+    (* We search recursively in the possible definitions of each free
+       variable. *)
+    let free_vars = Expr.free_vars e in
+    let possible_values_of_free_vars =
+      Var.Map.filter
+        (fun v _ -> Var.Set.mem v free_vars)
+        vc_scope_ctx.Conditions.vc_scope_possible_variable_values
+    in
+    Var.Map.fold
+      (fun _ possible_values vars_used ->
+        List.fold_left
+          (fun vars_used possible_value ->
+            Var.Set.union (vars_used_in_vc possible_value) vars_used)
+          vars_used possible_values)
+      possible_values_of_free_vars free_vars
+  in
+  let vars_used_in_vc = vars_used_in_vc vc.vc_guard in
   let vars_used_in_vc_with_known_values =
     Var.Set.filter
       (fun v ->
@@ -110,7 +128,7 @@ let solve_date_vc
           vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope)
       vars_used_in_vc
   in
-  Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values:@.%a@.%a"
+  Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values:@.%a%a%a"
     (Print.expr ()) vc.vc_guard (Print.expr ())
     vc_scope_ctx.Conditions.vc_scope_asserts
     (fun fmt vars_possible_values ->
@@ -133,12 +151,29 @@ let solve_date_vc
         ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
         (fun fmt var ->
           if Var.Set.mem var vars_used_in_vc_defined_outside_of_scope then (
+            Format.fprintf fmt "<OOS>";
+            Format.fprintf fmt "@[<hov 2>%a@ =@ unknown (out of scope)@]"
+              Print.var_debug var;
+            Format.fprintf fmt "</OOS>"))
+        fmt
+        (Var.Set.elements variables_defined_out_of_scope))
+    vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope
+    (fun fmt other_variables ->
+      Format.pp_print_list
+        ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+        (fun fmt var ->
+          if
+            not
+              (Var.Set.mem var vars_used_in_vc_defined_outside_of_scope
+              || Var.Set.mem var vars_used_in_vc_with_known_values)
+          then (
             Format.fprintf fmt "<UNK>";
-            Format.fprintf fmt "@[<hov 2>%a@ =@ unknown@]" Print.var_debug var;
+            Format.fprintf fmt "@[<hov 2>%a@ =@ unknown (others)@]"
+              Print.var_debug var;
             Format.fprintf fmt "</UNK>"))
         fmt
-        (Var.Set.elements variables_defined_out_of_scope))
-    vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope;
+        (Var.Set.elements other_variables))
+    vars_used_in_vc;
   let prog = turn_vc_into_mopsa_compatible_program vc in
   let prog_string =
     Var.Map.fold

From bcc2a215a742c8c3815d1bc943e91d403ecd4530 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Fri, 23 Jun 2023 14:17:02 +0200
Subject: [PATCH 13/31] WIP on Catala/Mopsa-dates connection: program
 generation is almost complete, we just lack some type annotations

---
 compiler/shared_ast/var.ml      |   1 +
 compiler/shared_ast/var.mli     |   1 +
 compiler/verification/solver.ml | 194 ++++++++++++++++----------------
 3 files changed, 100 insertions(+), 96 deletions(-)

diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index 5eeafe189..738e633ae 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -79,6 +79,7 @@ module Set = struct
   let choose_opt s = Option.map get (choose_opt s)
   let filter f s = filter (fun v -> f (get v)) s
   let exists f s = exists (fun v -> f (get v)) s
+  let inter s1 s2 = inter s1 s2
 
   (* Add more as needed *)
 end
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index 9bbb27edf..20628f5c3 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -52,6 +52,7 @@ module Set : sig
   val choose_opt : 'e t -> 'e var option
   val filter : ('e var -> bool) -> 'e t -> 'e t
   val exists : ('e var -> bool) -> 'e t -> bool
+  val inter : 'e t -> 'e t -> 'e t
 end
 
 (** Wrapper over [Map.S] but with a type variable for the AST type parameters.
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 095269535..b80adf91d 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -17,30 +17,93 @@
 open Catala_utils
 open Shared_ast
 
+let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
+  typed Dcalc.Ast.expr Var.Set.t =
+  (* We search recursively in the possible definitions of each free
+     variable. *)
+  let free_vars = Expr.free_vars e in
+  let possible_values_of_free_vars =
+    Var.Map.filter
+      (fun v _ -> Var.Set.mem v free_vars)
+      vc_scope_ctx.Conditions.vc_scope_possible_variable_values
+  in
+  Var.Map.fold
+    (fun _ possible_values vars_used ->
+       List.fold_left
+         (fun vars_used possible_value ->
+            Var.Set.union (vars_used_in_vc vc_scope_ctx possible_value) vars_used)
+         vars_used possible_values)
+    possible_values_of_free_vars free_vars
+
 module TypedValuesDcalcVarMap = struct
-  type 'x t = (typed Dcalc.Ast.expr, ('x, typed) marked) Var.Map.t
+  type 'x t = (typed Dcalc.Ast.expr, (('x, typed) marked) option) Var.Map.t
 
   let map (f : 'a -> 'b) (m : 'a t) : 'b t =
-    Var.Map.map (fun (x, tx) -> f x, tx) m
+    Var.Map.map (Option.map (fun (x, tx) -> f x, tx)) m
 end
 
 module TypedValuesDcalcVarMapBoxLifting = Bindlib.Lift (TypedValuesDcalcVarMap)
 
 type mopsa_program = {
   main_guard : typed Dcalc.Ast.expr;
-  other_values : (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr) Var.Map.t;
+  declared_variables :
+    ((dcalc, typed) gexpr Var.t * typed Dcalc.Ast.expr option) list;
+        (* ((typed Dcalc.Ast.expr * (typed Dcalc.Ast.expr) option)) list; *)
 }
 
 (* The goal of this part is to extract additions from expressions, and perform
    them before as assignments. This will simplify the analysis and communication
    with Mopsa. *)
 let turn_vc_into_mopsa_compatible_program
-    (vc : Conditions.verification_condition) : mopsa_program =
+    (vc : Conditions.verification_condition) vc_scope_ctx : mopsa_program =
+  let vars_used_in_vc = vars_used_in_vc vc_scope_ctx vc.vc_guard in
+  let vars_used_in_vc_with_known_values =
+    Var.Set.filter
+      (fun v ->
+         Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
+      vars_used_in_vc
+  in
+  let vars_used_in_vc_defined_outside_of_scope =
+    Var.Set.inter
+      vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope
+      vars_used_in_vc
+  in
+  let decls_to_top =
+    let others =
+      Var.Set.diff
+        vars_used_in_vc
+        (Var.Set.union
+           vars_used_in_vc_defined_outside_of_scope
+           vars_used_in_vc_with_known_values) in
+    List.fold_left (fun decls v -> (v, None)::decls) [] (Var.Set.elements (Var.Set.union vars_used_in_vc_defined_outside_of_scope others))
+  in
+  let assignments =
+    List.fold_left (fun decls (var, values) ->
+        if Var.Set.mem var vars_used_in_vc_with_known_values then
+          (* FIXME handle multiple values *)
+          let () = assert((List.length values) = 1) in
+          (var, (Some (List.hd values)))::decls
+        else
+          decls
+      ) []
+      (Var.Map.bindings vc_scope_ctx.vc_scope_possible_variable_values) in
+  let declared_variables = decls_to_top @ assignments in 
   let trivial_map_union = Var.Map.union (fun _ _ _ -> assert false) in
+  let rec transform_field_accesses_into_variables e =
+    match Mark.remove e with
+    | EStructAccess
+        { e = (EVar v, _); } when List.exists (fun (v2, _) -> Var.compare v v2 = 0) declared_variables ->
+      Message.emit_debug "Variable %a in assignements, but we may need to patch with %a" Print.var v (Print.expr ()) e;
+      let var = Var.make (Format.asprintf "%a" (Print.expr ()) e) in
+      Var.Map.singleton var None, Expr.evar var (Mark.get e)
+    | _ ->
+      Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union
+        ~f:transform_field_accesses_into_variables e
+  in
   let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
-      (typed Dcalc.Ast.expr, (dcalc, typed) boxed_gexpr) Var.Map.t
+      (typed Dcalc.Ast.expr, ((dcalc, typed) boxed_gexpr) option) Var.Map.t
       * (dcalc, typed) boxed_gexpr =
-    match Mark.remove e with
+    match Mark.remove e with 
     | EApp
         {
           f =
@@ -66,13 +129,22 @@ let turn_vc_into_mopsa_compatible_program
              (Pos.get_end_line pos) (Pos.get_end_column pos))
       in
       let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
-      Var.Map.add dummy_var new_e acc, Expr.evar dummy_var (Mark.get e)
+      Var.Map.add dummy_var (Some new_e) acc, Expr.evar dummy_var (Mark.get e)
     | _ ->
       Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union
         ~f:split_expression_into_atomic_parts e
   in
+  let new_vars_fields, (e, e_mark) =
+    transform_field_accesses_into_variables vc.vc_guard in
+  let new_vars_fields, e =
+    Bindlib.unbox
+      (Bindlib.box_apply2
+         (fun new_vars e ->
+            new_vars, (e, e_mark))
+         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars_fields)
+         e) in
   let new_vars, (simple_guard, simple_guard_mark) =
-    split_expression_into_atomic_parts vc.vc_guard
+    split_expression_into_atomic_parts e
   in
   let new_vars, simple_guard =
     (* This manipulation is done so that we only unbox once to keep all
@@ -82,9 +154,11 @@ let turn_vc_into_mopsa_compatible_program
          (fun new_vars simple_guard ->
            new_vars, (simple_guard, simple_guard_mark))
          (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars)
-         simple_guard)
-  in
-  { main_guard = simple_guard; other_values = new_vars }
+         simple_guard) in
+  {
+    main_guard = simple_guard;
+    declared_variables = declared_variables @ (Var.Map.bindings new_vars_fields) @ (Var.Map.bindings new_vars)
+  }
 
 (** This function is temporarily here but should be moved to a MOPSA backend. *)
 let solve_date_vc
@@ -96,92 +170,20 @@ let solve_date_vc
     (Z3backend.Io.print_negative_result vc scope_name
        (Z3backend.Io.make_context decl_ctx)
        None);
-  let rec vars_used_in_vc (e : typed Dcalc.Ast.expr) :
-      typed Dcalc.Ast.expr Var.Set.t =
-    (* We search recursively in the possible definitions of each free
-       variable. *)
-    let free_vars = Expr.free_vars e in
-    let possible_values_of_free_vars =
-      Var.Map.filter
-        (fun v _ -> Var.Set.mem v free_vars)
-        vc_scope_ctx.Conditions.vc_scope_possible_variable_values
-    in
-    Var.Map.fold
-      (fun _ possible_values vars_used ->
-        List.fold_left
-          (fun vars_used possible_value ->
-            Var.Set.union (vars_used_in_vc possible_value) vars_used)
-          vars_used possible_values)
-      possible_values_of_free_vars free_vars
-  in
-  let vars_used_in_vc = vars_used_in_vc vc.vc_guard in
-  let vars_used_in_vc_with_known_values =
-    Var.Set.filter
-      (fun v ->
-        Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
-      vars_used_in_vc
-  in
-  let vars_used_in_vc_defined_outside_of_scope =
-    Var.Set.filter
-      (fun v ->
-        Var.Set.mem v
-          vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope)
-      vars_used_in_vc
-  in
-  Message.emit_debug "For: %a@.Assumptions: %a@.Relevant values:@.%a%a%a"
-    (Print.expr ()) vc.vc_guard (Print.expr ())
-    vc_scope_ctx.Conditions.vc_scope_asserts
-    (fun fmt vars_possible_values ->
-      Format.pp_print_list
-        ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
-        (fun fmt (var, values) ->
-          if Var.Set.mem var vars_used_in_vc_with_known_values then (
-            Format.fprintf fmt "<IMP>";
-            Format.fprintf fmt "@[<hov 2>%a@ =@ %a@]" Print.var_debug var
-              (Format.pp_print_list
-                 ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
-                 (fun fmt expr -> Print.expr () fmt expr))
-              values;
-            Format.fprintf fmt "</IMP>"))
-        fmt
-        (Var.Map.bindings vars_possible_values))
-    vc_scope_ctx.Conditions.vc_scope_possible_variable_values
-    (fun fmt variables_defined_out_of_scope ->
-      Format.pp_print_list
-        ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
-        (fun fmt var ->
-          if Var.Set.mem var vars_used_in_vc_defined_outside_of_scope then (
-            Format.fprintf fmt "<OOS>";
-            Format.fprintf fmt "@[<hov 2>%a@ =@ unknown (out of scope)@]"
-              Print.var_debug var;
-            Format.fprintf fmt "</OOS>"))
-        fmt
-        (Var.Set.elements variables_defined_out_of_scope))
-    vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope
-    (fun fmt other_variables ->
-      Format.pp_print_list
-        ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
-        (fun fmt var ->
-          if
-            not
-              (Var.Set.mem var vars_used_in_vc_defined_outside_of_scope
-              || Var.Set.mem var vars_used_in_vc_with_known_values)
-          then (
-            Format.fprintf fmt "<UNK>";
-            Format.fprintf fmt "@[<hov 2>%a@ =@ unknown (others)@]"
-              Print.var_debug var;
-            Format.fprintf fmt "</UNK>"))
-        fmt
-        (Var.Set.elements other_variables))
-    vars_used_in_vc;
-  let prog = turn_vc_into_mopsa_compatible_program vc in
+  let prog = turn_vc_into_mopsa_compatible_program vc vc_scope_ctx in
   let prog_string =
-    Var.Map.fold
-      (fun var expr acc ->
-        Format.asprintf "%a %a = %a@." (Print.typ decl_ctx) (Expr.ty expr)
-          Print.var_debug var (Print.expr ()) expr
-        ^ acc)
-      prog.other_values ""
+    List.fold_left
+      (fun acc (var, oexpr) ->
+         acc^(match oexpr with
+         | None ->
+           (* FIXME typ *)
+           (* let (Typed { ty = match_ty; _ }) = Mark.get var in *)
+           Format.asprintf "%a = T@." (*(Print.typ decl_ctx) (Expr.ty )*) Print.var_debug var
+         | Some expr ->
+           Format.asprintf "%a %a = %a@." (Print.typ decl_ctx) (Expr.ty expr)
+             Print.var_debug var (Print.expr ()) expr)
+      )
+      "" prog.declared_variables
     ^ Format.asprintf "assert(sync(%a))" (Print.expr ()) prog.main_guard
   in
   Format.eprintf "Prog:@.%s@." prog_string

From b08841e7546f0caac3b5cf4cf71912a116d6a7b6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Fri, 23 Jun 2023 16:42:58 +0200
Subject: [PATCH 14/31] Verification conditions, track variables typs more
 accurately

---
 compiler/verification/conditions.ml  | 7 ++++++-
 compiler/verification/conditions.mli | 1 +
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index 03a2fb9c1..aefbc529b 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -387,6 +387,8 @@ let rec generate_verification_conditions_scope_body_expr
             ctx with
             scope_cond_input_vars =
               Var.Set.add scope_let_var ctx.scope_cond_input_vars;
+            scope_cond_variables_typs =
+              Var.Map.add scope_let_var scope_let.scope_let_typ ctx.scope_cond_variables_typs ;
           },
           [] )
       | DestructuringSubScopeResults ->
@@ -394,7 +396,8 @@ let rec generate_verification_conditions_scope_body_expr
             ctx with
             scope_cond_subscope_output_vars =
               Var.Set.add scope_let_var ctx.scope_cond_subscope_output_vars;
-          },
+            scope_cond_variables_typs =
+              Var.Map.add scope_let_var scope_let.scope_let_typ ctx.scope_cond_variables_typs ;          },
           [] )
       | ScopeVarDefinition | SubScopeVarDefinition ->
         (* For scope variables, we should check both that they never evaluate to
@@ -498,6 +501,7 @@ type verification_conditions_scope = {
     (typed Dcalc.Ast.expr, typed Dcalc.Ast.expr list) Var.Map.t;
   vc_scope_variables_defined_outside_of_scope : typed Dcalc.Ast.expr Var.Set.t;
   vc_scope_list : verification_condition list;
+  vc_scope_variables_typs : (typed expr, typ) Var.Map.t;
 }
 
 let generate_verification_conditions_code_items
@@ -550,6 +554,7 @@ let generate_verification_conditions_code_items
               vc_scope_variables_defined_outside_of_scope =
                 Var.Set.union ctx.scope_cond_input_vars
                   ctx.scope_cond_subscope_output_vars;
+              vc_scope_variables_typs = ctx.scope_cond_variables_typs;
             }
             vcs
         else vcs)
diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli
index b67b354e5..e994847db 100644
--- a/compiler/verification/conditions.mli
+++ b/compiler/verification/conditions.mli
@@ -49,6 +49,7 @@ type verification_conditions_scope = {
           traversal of the default tree. *)
   vc_scope_variables_defined_outside_of_scope : typed Dcalc.Ast.expr Var.Set.t;
   vc_scope_list : verification_condition list;
+  vc_scope_variables_typs : (typed Dcalc.Ast.expr, typ) Var.Map.t;
 }
 
 val generate_verification_conditions :

From d61123c98356770ed6f102f63d496520980e1fbf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Fri, 23 Jun 2023 16:43:10 +0200
Subject: [PATCH 15/31] Alpha version of Mopsa-compatible program generation

---
 compiler/verification/solver.ml | 93 +++++++++++++++++++++------------
 1 file changed, 61 insertions(+), 32 deletions(-)

diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index b80adf91d..c84dbea33 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -17,6 +17,14 @@
 open Catala_utils
 open Shared_ast
 
+let simplified_string_of_pos pos =
+  let basename =
+    Filename.basename (Pos.get_file pos) |> Filename.chop_extension
+  in
+  Format.asprintf "%s_%d-%d_%d-%d" basename
+    (Pos.get_start_line pos) (Pos.get_start_column pos)
+    (Pos.get_end_line pos) (Pos.get_end_column pos)
+
 let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
   typed Dcalc.Ast.expr Var.Set.t =
   (* We search recursively in the possible definitions of each free
@@ -55,7 +63,9 @@ type mopsa_program = {
    them before as assignments. This will simplify the analysis and communication
    with Mopsa. *)
 let turn_vc_into_mopsa_compatible_program
-    (vc : Conditions.verification_condition) vc_scope_ctx : mopsa_program =
+    (vc : Conditions.verification_condition)
+    (vc_scope_ctx : Conditions.verification_conditions_scope) :
+  mopsa_program * Conditions.verification_conditions_scope =
   let vars_used_in_vc = vars_used_in_vc vc_scope_ctx vc.vc_guard in
   let vars_used_in_vc_with_known_values =
     Var.Set.filter
@@ -88,16 +98,14 @@ let turn_vc_into_mopsa_compatible_program
       ) []
       (Var.Map.bindings vc_scope_ctx.vc_scope_possible_variable_values) in
   let declared_variables = decls_to_top @ assignments in 
-  let trivial_map_union = Var.Map.union (fun _ _ _ -> assert false) in
   let rec transform_field_accesses_into_variables e =
     match Mark.remove e with
     | EStructAccess
-        { e = (EVar v, _); } when List.exists (fun (v2, _) -> Var.compare v v2 = 0) declared_variables ->
-      Message.emit_debug "Variable %a in assignements, but we may need to patch with %a" Print.var v (Print.expr ()) e;
+        { e = (EVar v, _); _; } when List.exists (fun (v2, _) -> Var.compare v v2 = 0) declared_variables ->
       let var = Var.make (Format.asprintf "%a" (Print.expr ()) e) in
-      Var.Map.singleton var None, Expr.evar var (Mark.get e)
+      Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
     | _ ->
-      Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union
+      Expr.map_gather ~acc:Var.Map.empty ~join:(Var.Map.union (fun _ _ _ -> assert false))
         ~f:transform_field_accesses_into_variables e
   in
   let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
@@ -115,27 +123,30 @@ let turn_vc_into_mopsa_compatible_program
         List.fold_left_map
           (fun acc arg ->
             let toadd, arg = split_expression_into_atomic_parts arg in
-            trivial_map_union acc toadd, arg)
+            (Var.Map.union (fun _ _ _ -> assert false)) acc toadd, arg)
           Var.Map.empty args
       in
       let dummy_var =
         let pos = Expr.pos e in
-        let basename =
-          Filename.basename (Pos.get_file pos) |> Filename.chop_extension
-        in
         Var.make
-          (Format.asprintf "var_%s_%d-%d_%d-%d" basename
-             (Pos.get_start_line pos) (Pos.get_start_column pos)
-             (Pos.get_end_line pos) (Pos.get_end_column pos))
+          ("var_" ^ (simplified_string_of_pos pos))
       in
       let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
       Var.Map.add dummy_var (Some new_e) acc, Expr.evar dummy_var (Mark.get e)
     | _ ->
-      Expr.map_gather ~acc:Var.Map.empty ~join:trivial_map_union
+      Expr.map_gather ~acc:Var.Map.empty ~join:(Var.Map.union (fun _ _ _ -> assert false))
         ~f:split_expression_into_atomic_parts e
   in
   let new_vars_fields, (e, e_mark) =
     transform_field_accesses_into_variables vc.vc_guard in
+  let new_vars_fields, vc_scope_ctx =
+    Var.Map.map (fun _ -> None) new_vars_fields,
+    {
+      vc_scope_ctx with vc_scope_variables_typs =
+                         Var.Map.union (fun _ _ _ -> assert false)
+                           vc_scope_ctx.vc_scope_variables_typs
+                           new_vars_fields 
+    } in
   let new_vars_fields, e =
     Bindlib.unbox
       (Bindlib.box_apply2
@@ -157,8 +168,8 @@ let turn_vc_into_mopsa_compatible_program
          simple_guard) in
   {
     main_guard = simple_guard;
-    declared_variables = declared_variables @ (Var.Map.bindings new_vars_fields) @ (Var.Map.bindings new_vars)
-  }
+    declared_variables = declared_variables @ (Var.Map.bindings new_vars_fields) @ (List.rev @@ Var.Map.bindings new_vars)
+  }, vc_scope_ctx
 
 (** This function is temporarily here but should be moved to a MOPSA backend. *)
 let solve_date_vc
@@ -170,23 +181,41 @@ let solve_date_vc
     (Z3backend.Io.print_negative_result vc scope_name
        (Z3backend.Io.make_context decl_ctx)
        None);
-  let prog = turn_vc_into_mopsa_compatible_program vc vc_scope_ctx in
-  let prog_string =
-    List.fold_left
-      (fun acc (var, oexpr) ->
-         acc^(match oexpr with
-         | None ->
-           (* FIXME typ *)
-           (* let (Typed { ty = match_ty; _ }) = Mark.get var in *)
-           Format.asprintf "%a = T@." (*(Print.typ decl_ctx) (Expr.ty )*) Print.var_debug var
-         | Some expr ->
-           Format.asprintf "%a %a = %a@." (Print.typ decl_ctx) (Expr.ty expr)
-             Print.var_debug var (Print.expr ()) expr)
+  let prog, vc_scope_ctx = turn_vc_into_mopsa_compatible_program vc vc_scope_ctx in
+  let prog_name = "proof_obligation_" ^ (simplified_string_of_pos (Expr.pos prog.main_guard)) ^ ".u" in
+  let prog_channel = open_out prog_name in
+  let fmt = Format.formatter_of_out_channel prog_channel in
+  let () = Format.pp_set_margin fmt 2000 in
+  let () = Format.fprintf fmt "%aassert(sync(%s));@."
+      (Format.pp_print_list
+         ~pp_sep:(fun _ () -> ())
+         (fun fmt (var, oexpr) ->
+            match oexpr with
+            | None ->
+              begin match Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs with
+                | None ->
+                  (* This should only correspond to structures that are not accessed, so we can skip *)
+                  Message.emit_warning "Ignoring type declaration of var %a, as we've lost its type" Print.var_debug var 
+                | Some ty ->
+                  let make_random = match Mark.remove ty with
+                    | TLit TDate -> "date()"
+                    | TLit TDuration -> "duration_ym()"
+                    | TLit TBool -> "bool()"
+                    | TLit TInt -> "int()"
+                    | _ -> failwith "not implemented" in
+                  Format.fprintf fmt "%a %s = make_random_%s;@." (Print.typ decl_ctx) ty
+                    (String.to_ascii @@ Format.asprintf "%a" Print.var var) make_random 
+              end
+            | Some expr ->
+              Format.fprintf fmt "%a %s = %s;@." (Print.typ decl_ctx) (Expr.ty expr)
+                (String.to_ascii @@ Format.asprintf "%a" Print.var var)
+                (String.to_ascii @@ Format.asprintf "%a" (Print.expr ~debug:false ()) expr)
+         )
       )
-      "" prog.declared_variables
-    ^ Format.asprintf "assert(sync(%a))" (Print.expr ()) prog.main_guard
-  in
-  Format.eprintf "Prog:@.%s@." prog_string
+      prog.declared_variables
+      (String.to_ascii @@ Format.asprintf "%a" (Print.expr ~debug:false ()) prog.main_guard) in
+  close_out prog_channel;
+  Message.emit_debug "Generated new Mopsa program at %s" prog_name
 
 (** [solve_vc] is the main entry point of this module. It takes a list of
     expressions [vcs] corresponding to verification conditions that must be

From e2bf3cc99f7e0629c3c042ae259167f352fde899 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Fri, 23 Jun 2023 16:55:09 +0200
Subject: [PATCH 16/31] Format code

---
 compiler/verification/conditions.ml |   7 +-
 compiler/verification/solver.ml     | 187 ++++++++++++++++------------
 2 files changed, 114 insertions(+), 80 deletions(-)

diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml
index aefbc529b..750222159 100644
--- a/compiler/verification/conditions.ml
+++ b/compiler/verification/conditions.ml
@@ -388,7 +388,8 @@ let rec generate_verification_conditions_scope_body_expr
             scope_cond_input_vars =
               Var.Set.add scope_let_var ctx.scope_cond_input_vars;
             scope_cond_variables_typs =
-              Var.Map.add scope_let_var scope_let.scope_let_typ ctx.scope_cond_variables_typs ;
+              Var.Map.add scope_let_var scope_let.scope_let_typ
+                ctx.scope_cond_variables_typs;
           },
           [] )
       | DestructuringSubScopeResults ->
@@ -397,7 +398,9 @@ let rec generate_verification_conditions_scope_body_expr
             scope_cond_subscope_output_vars =
               Var.Set.add scope_let_var ctx.scope_cond_subscope_output_vars;
             scope_cond_variables_typs =
-              Var.Map.add scope_let_var scope_let.scope_let_typ ctx.scope_cond_variables_typs ;          },
+              Var.Map.add scope_let_var scope_let.scope_let_typ
+                ctx.scope_cond_variables_typs;
+          },
           [] )
       | ScopeVarDefinition | SubScopeVarDefinition ->
         (* For scope variables, we should check both that they never evaluate to
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index c84dbea33..fae97b243 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -21,14 +21,12 @@ let simplified_string_of_pos pos =
   let basename =
     Filename.basename (Pos.get_file pos) |> Filename.chop_extension
   in
-  Format.asprintf "%s_%d-%d_%d-%d" basename
-    (Pos.get_start_line pos) (Pos.get_start_column pos)
-    (Pos.get_end_line pos) (Pos.get_end_column pos)
+  Format.asprintf "%s_%d-%d_%d-%d" basename (Pos.get_start_line pos)
+    (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
 
 let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
-  typed Dcalc.Ast.expr Var.Set.t =
-  (* We search recursively in the possible definitions of each free
-     variable. *)
+    typed Dcalc.Ast.expr Var.Set.t =
+  (* We search recursively in the possible definitions of each free variable. *)
   let free_vars = Expr.free_vars e in
   let possible_values_of_free_vars =
     Var.Map.filter
@@ -37,14 +35,14 @@ let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
   in
   Var.Map.fold
     (fun _ possible_values vars_used ->
-       List.fold_left
-         (fun vars_used possible_value ->
-            Var.Set.union (vars_used_in_vc vc_scope_ctx possible_value) vars_used)
-         vars_used possible_values)
+      List.fold_left
+        (fun vars_used possible_value ->
+          Var.Set.union (vars_used_in_vc vc_scope_ctx possible_value) vars_used)
+        vars_used possible_values)
     possible_values_of_free_vars free_vars
 
 module TypedValuesDcalcVarMap = struct
-  type 'x t = (typed Dcalc.Ast.expr, (('x, typed) marked) option) Var.Map.t
+  type 'x t = (typed Dcalc.Ast.expr, ('x, typed) marked option) Var.Map.t
 
   let map (f : 'a -> 'b) (m : 'a t) : 'b t =
     Var.Map.map (Option.map (fun (x, tx) -> f x, tx)) m
@@ -56,7 +54,7 @@ type mopsa_program = {
   main_guard : typed Dcalc.Ast.expr;
   declared_variables :
     ((dcalc, typed) gexpr Var.t * typed Dcalc.Ast.expr option) list;
-        (* ((typed Dcalc.Ast.expr * (typed Dcalc.Ast.expr) option)) list; *)
+      (* ((typed Dcalc.Ast.expr * (typed Dcalc.Ast.expr) option)) list; *)
 }
 
 (* The goal of this part is to extract additions from expressions, and perform
@@ -65,12 +63,12 @@ type mopsa_program = {
 let turn_vc_into_mopsa_compatible_program
     (vc : Conditions.verification_condition)
     (vc_scope_ctx : Conditions.verification_conditions_scope) :
-  mopsa_program * Conditions.verification_conditions_scope =
+    mopsa_program * Conditions.verification_conditions_scope =
   let vars_used_in_vc = vars_used_in_vc vc_scope_ctx vc.vc_guard in
   let vars_used_in_vc_with_known_values =
     Var.Set.filter
       (fun v ->
-         Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
+        Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
       vars_used_in_vc
   in
   let vars_used_in_vc_defined_outside_of_scope =
@@ -80,38 +78,44 @@ let turn_vc_into_mopsa_compatible_program
   in
   let decls_to_top =
     let others =
-      Var.Set.diff
-        vars_used_in_vc
-        (Var.Set.union
-           vars_used_in_vc_defined_outside_of_scope
-           vars_used_in_vc_with_known_values) in
-    List.fold_left (fun decls v -> (v, None)::decls) [] (Var.Set.elements (Var.Set.union vars_used_in_vc_defined_outside_of_scope others))
+      Var.Set.diff vars_used_in_vc
+        (Var.Set.union vars_used_in_vc_defined_outside_of_scope
+           vars_used_in_vc_with_known_values)
+    in
+    List.fold_left
+      (fun decls v -> (v, None) :: decls)
+      []
+      (Var.Set.elements
+         (Var.Set.union vars_used_in_vc_defined_outside_of_scope others))
   in
   let assignments =
-    List.fold_left (fun decls (var, values) ->
+    List.fold_left
+      (fun decls (var, values) ->
         if Var.Set.mem var vars_used_in_vc_with_known_values then
           (* FIXME handle multiple values *)
-          let () = assert((List.length values) = 1) in
-          (var, (Some (List.hd values)))::decls
-        else
-          decls
-      ) []
-      (Var.Map.bindings vc_scope_ctx.vc_scope_possible_variable_values) in
-  let declared_variables = decls_to_top @ assignments in 
+          let () = assert (List.length values = 1) in
+          (var, Some (List.hd values)) :: decls
+        else decls)
+      []
+      (Var.Map.bindings vc_scope_ctx.vc_scope_possible_variable_values)
+  in
+  let declared_variables = decls_to_top @ assignments in
   let rec transform_field_accesses_into_variables e =
     match Mark.remove e with
-    | EStructAccess
-        { e = (EVar v, _); _; } when List.exists (fun (v2, _) -> Var.compare v v2 = 0) declared_variables ->
+    | EStructAccess { e = EVar v, _; _ }
+      when List.exists (fun (v2, _) -> Var.compare v v2 = 0) declared_variables
+      ->
       let var = Var.make (Format.asprintf "%a" (Print.expr ()) e) in
       Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
     | _ ->
-      Expr.map_gather ~acc:Var.Map.empty ~join:(Var.Map.union (fun _ _ _ -> assert false))
+      Expr.map_gather ~acc:Var.Map.empty
+        ~join:(Var.Map.union (fun _ _ _ -> assert false))
         ~f:transform_field_accesses_into_variables e
   in
   let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
-      (typed Dcalc.Ast.expr, ((dcalc, typed) boxed_gexpr) option) Var.Map.t
+      (typed Dcalc.Ast.expr, (dcalc, typed) boxed_gexpr option) Var.Map.t
       * (dcalc, typed) boxed_gexpr =
-    match Mark.remove e with 
+    match Mark.remove e with
     | EApp
         {
           f =
@@ -128,32 +132,35 @@ let turn_vc_into_mopsa_compatible_program
       in
       let dummy_var =
         let pos = Expr.pos e in
-        Var.make
-          ("var_" ^ (simplified_string_of_pos pos))
+        Var.make ("var_" ^ simplified_string_of_pos pos)
       in
       let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
       Var.Map.add dummy_var (Some new_e) acc, Expr.evar dummy_var (Mark.get e)
     | _ ->
-      Expr.map_gather ~acc:Var.Map.empty ~join:(Var.Map.union (fun _ _ _ -> assert false))
+      Expr.map_gather ~acc:Var.Map.empty
+        ~join:(Var.Map.union (fun _ _ _ -> assert false))
         ~f:split_expression_into_atomic_parts e
   in
   let new_vars_fields, (e, e_mark) =
-    transform_field_accesses_into_variables vc.vc_guard in
+    transform_field_accesses_into_variables vc.vc_guard
+  in
   let new_vars_fields, vc_scope_ctx =
-    Var.Map.map (fun _ -> None) new_vars_fields,
-    {
-      vc_scope_ctx with vc_scope_variables_typs =
-                         Var.Map.union (fun _ _ _ -> assert false)
-                           vc_scope_ctx.vc_scope_variables_typs
-                           new_vars_fields 
-    } in
+    ( Var.Map.map (fun _ -> None) new_vars_fields,
+      {
+        vc_scope_ctx with
+        vc_scope_variables_typs =
+          Var.Map.union
+            (fun _ _ _ -> assert false)
+            vc_scope_ctx.vc_scope_variables_typs new_vars_fields;
+      } )
+  in
   let new_vars_fields, e =
     Bindlib.unbox
       (Bindlib.box_apply2
-         (fun new_vars e ->
-            new_vars, (e, e_mark))
+         (fun new_vars e -> new_vars, (e, e_mark))
          (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars_fields)
-         e) in
+         e)
+  in
   let new_vars, (simple_guard, simple_guard_mark) =
     split_expression_into_atomic_parts e
   in
@@ -165,11 +172,17 @@ let turn_vc_into_mopsa_compatible_program
          (fun new_vars simple_guard ->
            new_vars, (simple_guard, simple_guard_mark))
          (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars)
-         simple_guard) in
-  {
-    main_guard = simple_guard;
-    declared_variables = declared_variables @ (Var.Map.bindings new_vars_fields) @ (List.rev @@ Var.Map.bindings new_vars)
-  }, vc_scope_ctx
+         simple_guard)
+  in
+  ( {
+      main_guard = simple_guard;
+      declared_variables =
+        declared_variables
+        @ Var.Map.bindings new_vars_fields
+        @ List.rev
+        @@ Var.Map.bindings new_vars;
+    },
+    vc_scope_ctx )
 
 (** This function is temporarily here but should be moved to a MOPSA backend. *)
 let solve_date_vc
@@ -181,39 +194,57 @@ let solve_date_vc
     (Z3backend.Io.print_negative_result vc scope_name
        (Z3backend.Io.make_context decl_ctx)
        None);
-  let prog, vc_scope_ctx = turn_vc_into_mopsa_compatible_program vc vc_scope_ctx in
-  let prog_name = "proof_obligation_" ^ (simplified_string_of_pos (Expr.pos prog.main_guard)) ^ ".u" in
+  let prog, vc_scope_ctx =
+    turn_vc_into_mopsa_compatible_program vc vc_scope_ctx
+  in
+  let prog_name =
+    "proof_obligation_"
+    ^ simplified_string_of_pos (Expr.pos prog.main_guard)
+    ^ ".u"
+  in
   let prog_channel = open_out prog_name in
   let fmt = Format.formatter_of_out_channel prog_channel in
   let () = Format.pp_set_margin fmt 2000 in
-  let () = Format.fprintf fmt "%aassert(sync(%s));@."
+  let () =
+    Format.fprintf fmt "%aassert(sync(%s));@."
       (Format.pp_print_list
          ~pp_sep:(fun _ () -> ())
          (fun fmt (var, oexpr) ->
-            match oexpr with
-            | None ->
-              begin match Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs with
-                | None ->
-                  (* This should only correspond to structures that are not accessed, so we can skip *)
-                  Message.emit_warning "Ignoring type declaration of var %a, as we've lost its type" Print.var_debug var 
-                | Some ty ->
-                  let make_random = match Mark.remove ty with
-                    | TLit TDate -> "date()"
-                    | TLit TDuration -> "duration_ym()"
-                    | TLit TBool -> "bool()"
-                    | TLit TInt -> "int()"
-                    | _ -> failwith "not implemented" in
-                  Format.fprintf fmt "%a %s = make_random_%s;@." (Print.typ decl_ctx) ty
-                    (String.to_ascii @@ Format.asprintf "%a" Print.var var) make_random 
-              end
-            | Some expr ->
-              Format.fprintf fmt "%a %s = %s;@." (Print.typ decl_ctx) (Expr.ty expr)
-                (String.to_ascii @@ Format.asprintf "%a" Print.var var)
-                (String.to_ascii @@ Format.asprintf "%a" (Print.expr ~debug:false ()) expr)
-         )
-      )
+           match oexpr with
+           | None -> begin
+             match
+               Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs
+             with
+             | None ->
+               (* This should only correspond to structures that are not
+                  accessed, so we can skip *)
+               Message.emit_warning
+                 "Ignoring type declaration of var %a, as we've lost its type"
+                 Print.var_debug var
+             | Some ty ->
+               let make_random =
+                 match Mark.remove ty with
+                 | TLit TDate -> "date()"
+                 | TLit TDuration -> "duration_ym()"
+                 | TLit TBool -> "bool()"
+                 | TLit TInt -> "int()"
+                 | _ -> failwith "not implemented"
+               in
+               Format.fprintf fmt "%a %s = make_random_%s;@."
+                 (Print.typ decl_ctx) ty
+                 (String.to_ascii @@ Format.asprintf "%a" Print.var var)
+                 make_random
+           end
+           | Some expr ->
+             Format.fprintf fmt "%a %s = %s;@." (Print.typ decl_ctx)
+               (Expr.ty expr)
+               (String.to_ascii @@ Format.asprintf "%a" Print.var var)
+               (String.to_ascii
+               @@ Format.asprintf "%a" (Print.expr ~debug:false ()) expr)))
       prog.declared_variables
-      (String.to_ascii @@ Format.asprintf "%a" (Print.expr ~debug:false ()) prog.main_guard) in
+      (String.to_ascii
+      @@ Format.asprintf "%a" (Print.expr ~debug:false ()) prog.main_guard)
+  in
   close_out prog_channel;
   Message.emit_debug "Generated new Mopsa program at %s" prog_name
 

From 3e2a1ab426c15cddbec677b251ee7bdcd9532c11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Fri, 23 Jun 2023 17:43:28 +0200
Subject: [PATCH 17/31] Mopsa export: top init all necessary variables

---
 compiler/verification/solver.ml | 53 ++++++++++++++++++++-------------
 1 file changed, 33 insertions(+), 20 deletions(-)

diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index fae97b243..cb92f224a 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -211,30 +211,43 @@ let solve_date_vc
          ~pp_sep:(fun _ () -> ())
          (fun fmt (var, oexpr) ->
            match oexpr with
-           | None -> begin
-             match
-               Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs
-             with
              | None ->
-               (* This should only correspond to structures that are not
-                  accessed, so we can skip *)
-               Message.emit_warning
-                 "Ignoring type declaration of var %a, as we've lost its type"
-                 Print.var_debug var
-             | Some ty ->
+               let ty = 
+                 begin
+                   match
+                     Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs
+                   with
+                   | None ->
+                     (* FIXME: I may have added to many variables in vc_scope_variables_typs in commit b08841e7,
+                               the good way to do it would be to extract types of variables from the expression directly *)
+                     let rec find_type_of_var v e = match e with
+                       | EVar v', mark when Var.compare v v' = 0 -> [mark]
+                       | e -> Expr.shallow_fold (fun e acc -> (find_type_of_var v e) @ acc) e [] in
+                     let m = find_type_of_var var vc.vc_guard in
+                     let (Typed { ty; _ }) = List.hd m in
+                     ty 
+                   | Some ty -> ty
+                 end in
                let make_random =
                  match Mark.remove ty with
-                 | TLit TDate -> "date()"
-                 | TLit TDuration -> "duration_ym()"
-                 | TLit TBool -> "bool()"
-                 | TLit TInt -> "int()"
-                 | _ -> failwith "not implemented"
+                 | TLit TDate -> Some  "date()"
+                 | TLit TDuration -> Some "duration_ym()"
+                 | TLit TBool -> Some "bool()"
+                 | TLit TInt -> Some "int()"
+                 | _ -> None 
                in
-               Format.fprintf fmt "%a %s = make_random_%s;@."
-                 (Print.typ decl_ctx) ty
-                 (String.to_ascii @@ Format.asprintf "%a" Print.var var)
-                 make_random
-           end
+               begin match make_random with
+                 | Some make_random ->
+                   Format.fprintf fmt "%a %s = make_random_%s;@."
+                     (Print.typ decl_ctx) ty
+                     (String.to_ascii @@ Format.asprintf "%a" Print.var var)
+                     make_random
+                 | None ->
+                   Message.emit_warning
+                     "Ignoring type declaration of var %a : %a"
+                     Print.var_debug var
+                     Print.typ_debug ty
+               end
            | Some expr ->
              Format.fprintf fmt "%a %s = %s;@." (Print.typ decl_ctx)
                (Expr.ty expr)

From b062e1ed738be41679a0efb31df94520d1f2dbf0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Fri, 23 Jun 2023 17:44:41 +0200
Subject: [PATCH 18/31] Format

---
 compiler/verification/solver.ml | 75 +++++++++++++++++----------------
 1 file changed, 39 insertions(+), 36 deletions(-)

diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index cb92f224a..dd00322b8 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -211,43 +211,46 @@ let solve_date_vc
          ~pp_sep:(fun _ () -> ())
          (fun fmt (var, oexpr) ->
            match oexpr with
+           | None -> (
+             let ty =
+               match
+                 Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs
+               with
+               | None ->
+                 (* FIXME: I may have added to many variables in
+                    vc_scope_variables_typs in commit b08841e7, the good way to
+                    do it would be to extract types of variables from the
+                    expression directly *)
+                 let rec find_type_of_var v e =
+                   match e with
+                   | EVar v', mark when Var.compare v v' = 0 -> [mark]
+                   | e ->
+                     Expr.shallow_fold
+                       (fun e acc -> find_type_of_var v e @ acc)
+                       e []
+                 in
+                 let m = find_type_of_var var vc.vc_guard in
+                 let (Typed { ty; _ }) = List.hd m in
+                 ty
+               | Some ty -> ty
+             in
+             let make_random =
+               match Mark.remove ty with
+               | TLit TDate -> Some "date()"
+               | TLit TDuration -> Some "duration_ym()"
+               | TLit TBool -> Some "bool()"
+               | TLit TInt -> Some "int()"
+               | _ -> None
+             in
+             match make_random with
+             | Some make_random ->
+               Format.fprintf fmt "%a %s = make_random_%s;@."
+                 (Print.typ decl_ctx) ty
+                 (String.to_ascii @@ Format.asprintf "%a" Print.var var)
+                 make_random
              | None ->
-               let ty = 
-                 begin
-                   match
-                     Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs
-                   with
-                   | None ->
-                     (* FIXME: I may have added to many variables in vc_scope_variables_typs in commit b08841e7,
-                               the good way to do it would be to extract types of variables from the expression directly *)
-                     let rec find_type_of_var v e = match e with
-                       | EVar v', mark when Var.compare v v' = 0 -> [mark]
-                       | e -> Expr.shallow_fold (fun e acc -> (find_type_of_var v e) @ acc) e [] in
-                     let m = find_type_of_var var vc.vc_guard in
-                     let (Typed { ty; _ }) = List.hd m in
-                     ty 
-                   | Some ty -> ty
-                 end in
-               let make_random =
-                 match Mark.remove ty with
-                 | TLit TDate -> Some  "date()"
-                 | TLit TDuration -> Some "duration_ym()"
-                 | TLit TBool -> Some "bool()"
-                 | TLit TInt -> Some "int()"
-                 | _ -> None 
-               in
-               begin match make_random with
-                 | Some make_random ->
-                   Format.fprintf fmt "%a %s = make_random_%s;@."
-                     (Print.typ decl_ctx) ty
-                     (String.to_ascii @@ Format.asprintf "%a" Print.var var)
-                     make_random
-                 | None ->
-                   Message.emit_warning
-                     "Ignoring type declaration of var %a : %a"
-                     Print.var_debug var
-                     Print.typ_debug ty
-               end
+               Message.emit_warning "Ignoring type declaration of var %a : %a"
+                 Print.var_debug var Print.typ_debug ty)
            | Some expr ->
              Format.fprintf fmt "%a %s = %s;@." (Print.typ decl_ctx)
                (Expr.ty expr)

From 7fea73e506d2251d5bc5104eb93d3be29f94bf87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Sun, 25 Jun 2023 23:12:39 +0200
Subject: [PATCH 19/31] WIP On Mopsa Backend

---
 compiler/verification/dune                  |   9 +-
 compiler/verification/mopsabackend.dummy.ml |  41 +++
 compiler/verification/mopsabackend.real.ml  | 325 +++++++++++++++++++
 compiler/verification/solver.ml             | 328 +++-----------------
 4 files changed, 417 insertions(+), 286 deletions(-)
 create mode 100644 compiler/verification/mopsabackend.dummy.ml
 create mode 100644 compiler/verification/mopsabackend.real.ml

diff --git a/compiler/verification/dune b/compiler/verification/dune
index 56e493680..14fca1024 100644
--- a/compiler/verification/dune
+++ b/compiler/verification/dune
@@ -11,7 +11,14 @@
    z3backend.ml
    from
    (z3 -> z3backend.real.ml)
-   (-> z3backend.dummy.ml))))
+   (-> z3backend.dummy.ml))
+  (select
+   mopsabackend.ml
+   from
+   (mopsa.mopsa_analyzer -> mopsabackend.real.ml)
+   (-> mopsabackend.dummy.ml))
+ )
+)
 
 (documentation
  (package catala)
diff --git a/compiler/verification/mopsabackend.dummy.ml b/compiler/verification/mopsabackend.dummy.ml
new file mode 100644
index 000000000..ad8ab72e8
--- /dev/null
+++ b/compiler/verification/mopsabackend.dummy.ml
@@ -0,0 +1,41 @@
+(* This file is part of the Catala compiler, a specification language for tax
+   and social benefits computation rules. Copyright (C) 2023 Inria, contributor:
+   Raphaël Monat <raphael.monat@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not
+   use this file except in compliance with the License. You may obtain a copy of
+   the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+   WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
+   License for the specific language governing permissions and limitations under
+   the License. *)
+
+(** Replicating the interface, with no actual implementation for compiling
+    without the expected backend. All functions print an error message and exit *)
+
+let dummy () =
+  Catala_utils.Message.raise_error
+    "This instance of Catala is not linked with Mopsa."
+
+module Io = struct
+  let init_backend () = dummy ()
+
+  type backend_context = unit
+
+  let make_context _ = dummy ()
+
+  type vc_encoding = unit
+
+  let translate_expr _ _ = dummy ()
+  let encode_asserts _ _ = dummy ()
+
+  type model = unit
+  type vc_encoding_result = Success of model * model | Fail of string
+
+  let print_negative_result _ _ _ = dummy ()
+  let check_vc _ _ = dummy ()
+end
diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
new file mode 100644
index 000000000..7c2fe4c51
--- /dev/null
+++ b/compiler/verification/mopsabackend.real.ml
@@ -0,0 +1,325 @@
+(* This file is part of the Catala compiler, a specification language for tax
+   and social benefits computation rules. Copyright (C) 2023 Inria, contributors:
+   Raphaël Monat <raphael.monat@inria.fr>, Denis Merigoux <denis.merigoux@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not
+   use this file except in compliance with the License. You may obtain a copy of
+   the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+   WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
+   License for the specific language governing permissions and limitations under
+   the License. *)
+
+open Catala_utils
+open Shared_ast
+
+type mopsa_program = {
+  main_guard : typed Dcalc.Ast.expr;
+  declared_variables :
+    ((dcalc, typed) gexpr Var.t * typed Dcalc.Ast.expr option) list;
+}
+
+
+let simplified_string_of_pos pos =
+  let basename =
+    Filename.basename (Pos.get_file pos) |> Filename.chop_extension
+  in
+  Format.asprintf "%s_%d-%d_%d-%d" basename (Pos.get_start_line pos)
+    (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
+
+let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
+  typed Dcalc.Ast.expr Var.Set.t =
+  (* We search recursively in the possible definitions of each free variable. *)
+  let free_vars = Expr.free_vars e in
+  let possible_values_of_free_vars =
+    Var.Map.filter
+      (fun v _ -> Var.Set.mem v free_vars)
+      vc_scope_ctx.Conditions.vc_scope_possible_variable_values
+  in
+  Var.Map.fold
+    (fun _ possible_values vars_used ->
+       List.fold_left
+         (fun vars_used possible_value ->
+            Var.Set.union (vars_used_in_vc vc_scope_ctx possible_value) vars_used)
+         vars_used possible_values)
+    possible_values_of_free_vars free_vars
+
+module TypedValuesDcalcVarMap = struct
+  type 'x t = (typed Dcalc.Ast.expr, ('x, typed) marked option) Var.Map.t
+
+  let map (f : 'a -> 'b) (m : 'a t) : 'b t =
+    Var.Map.map (Option.map (fun (x, tx) -> f x, tx)) m
+end
+
+module TypedValuesDcalcVarMapBoxLifting = Bindlib.Lift (TypedValuesDcalcVarMap)
+
+
+(* The goal of this part is to extract additions from expressions, and perform
+   them before as assignments. This will simplify the analysis and communication
+   with Mopsa. *)
+let translate_expr vc_scope_ctx vc_guard =
+  let vars_used_in_vc = vars_used_in_vc vc_scope_ctx vc_guard in
+  let vars_used_in_vc_with_known_values =
+    Var.Set.filter
+      (fun v ->
+        Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
+      vars_used_in_vc
+  in
+  let vars_used_in_vc_defined_outside_of_scope =
+    Var.Set.inter
+      vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope
+      vars_used_in_vc
+  in
+  let decls_to_top =
+    let others =
+      Var.Set.diff vars_used_in_vc
+        (Var.Set.union vars_used_in_vc_defined_outside_of_scope
+           vars_used_in_vc_with_known_values)
+    in
+    List.fold_left
+      (fun decls v -> (v, None) :: decls)
+      []
+      (Var.Set.elements
+         (Var.Set.union vars_used_in_vc_defined_outside_of_scope others))
+  in
+  let assignments =
+    List.fold_left
+      (fun decls (var, values) ->
+        if Var.Set.mem var vars_used_in_vc_with_known_values then
+          (* FIXME handle multiple values *)
+          let () = assert (List.length values = 1) in
+          (var, Some (List.hd values)) :: decls
+        else decls)
+      []
+      (Var.Map.bindings vc_scope_ctx.vc_scope_possible_variable_values)
+  in
+  let declared_variables = decls_to_top @ assignments in
+  let rec transform_field_accesses_into_variables e =
+    match Mark.remove e with
+    | EStructAccess { e = EVar v, _; _ }
+      when List.exists (fun (v2, _) -> Var.compare v v2 = 0) declared_variables
+      ->
+      let var = Var.make (Format.asprintf "%a" (Print.expr ()) e) in
+      Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
+    | _ ->
+      Expr.map_gather ~acc:Var.Map.empty
+        ~join:(Var.Map.union (fun _ _ _ -> assert false))
+        ~f:transform_field_accesses_into_variables e
+  in
+  let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
+      (typed Dcalc.Ast.expr, (dcalc, typed) boxed_gexpr option) Var.Map.t
+      * (dcalc, typed) boxed_gexpr =
+    match Mark.remove e with
+    | EApp
+        {
+          f =
+            ( EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound | Op.FirstDayOfMonth; tys = _ },
+              _ ) as f;
+          args;
+        } ->
+      let acc, args =
+        List.fold_left_map
+          (fun acc arg ->
+            let toadd, arg = split_expression_into_atomic_parts arg in
+            (Var.Map.union (fun _ _ _ -> assert false)) acc toadd, arg)
+          Var.Map.empty args
+      in
+      let dummy_var =
+        let pos = Expr.pos e in
+        Var.make ("var_" ^ simplified_string_of_pos pos)
+      in
+      let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
+      Var.Map.add dummy_var (Some new_e) acc, Expr.evar dummy_var (Mark.get e)
+    | _ ->
+      Expr.map_gather ~acc:Var.Map.empty
+        ~join:(Var.Map.union (fun _ _ _ -> assert false))
+        ~f:split_expression_into_atomic_parts e
+  in
+  let new_vars_fields, (e, e_mark) =
+    transform_field_accesses_into_variables vc_guard
+  in
+  let new_vars_fields, vc_scope_ctx =
+    ( Var.Map.map (fun _ -> None) new_vars_fields,
+      {
+        vc_scope_ctx with
+        vc_scope_variables_typs =
+          Var.Map.union
+            (fun _ _ _ -> assert false)
+            vc_scope_ctx.vc_scope_variables_typs new_vars_fields;
+      } )
+  in
+  let new_vars_fields, e =
+    Bindlib.unbox
+      (Bindlib.box_apply2
+         (fun new_vars e -> new_vars, (e, e_mark))
+         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars_fields)
+         e)
+  in
+  let new_vars, (simple_guard, simple_guard_mark) =
+    split_expression_into_atomic_parts e
+  in
+  let new_vars, simple_guard =
+    (* This manipulation is done so that we only unbox once to keep all
+       variables in sync. *)
+    Bindlib.unbox
+      (Bindlib.box_apply2
+         (fun new_vars simple_guard ->
+           new_vars, (simple_guard, simple_guard_mark))
+         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars)
+         simple_guard)
+  in
+  (vc_scope_ctx,
+   {
+      main_guard = simple_guard;
+      declared_variables =
+        declared_variables
+        @ Var.Map.bindings new_vars_fields
+        @ List.rev
+        @@ Var.Map.bindings new_vars;
+    })
+
+
+
+let print_encoding (prog : mopsa_program) =
+  let fmt = Format.str_formatter in
+  let () =
+    Format.fprintf fmt "%aassert(sync(%a));@."
+      (Format.pp_print_list
+         ~pp_sep:(fun _ () -> ())
+         (fun fmt (var, oexpr) ->
+           match oexpr with
+           | None -> (
+             let ty =
+               let rec find_type_of_var v e =
+                 match e with
+                 | EVar v', mark when Var.compare v v' = 0 -> [mark]
+                 | e ->
+                   Expr.shallow_fold
+                     (fun e acc -> find_type_of_var v e @ acc)
+                     e []
+               in
+               let m = find_type_of_var var prog.main_guard in 
+               let (Typed { ty; _ }) = List.hd m in
+               ty in
+             (*     match *)
+             (*     Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs *)
+             (*   with *)
+             (*   | None -> *)
+             (*     (\* FIXME: I may have added to many variables in *)
+             (*        vc_scope_variables_typs in commit b08841e7, the good way to *)
+             (*        do it would be to extract types of variables from the *)
+             (*        expression directly *\) *)
+             (*   | Some ty -> ty *)
+             (* in *)
+             let make_random =
+               match Mark.remove ty with
+               | TLit TDate -> Some "date()"
+               | TLit TDuration -> Some "duration_ym()"
+               | TLit TBool -> Some "bool()"
+               | TLit TInt -> Some "int()"
+               | _ -> None
+             in
+             match make_random with
+             | Some make_random ->
+               Format.fprintf fmt "%a %a = make_random_%s;@."
+                 Print.typ_debug ty
+                 Print.var var
+                 make_random
+             | None ->
+               Message.emit_warning "Ignoring type declaration of var %a : %a"
+                 Print.var_debug var Print.typ_debug ty)
+           | Some expr ->
+             Format.fprintf fmt "%a %a = %a;@."
+               Print.typ_debug (Expr.ty expr)
+               Print.var var
+               (Print.expr ~debug:false ()) expr))
+      prog.declared_variables
+      (Print.expr ~debug:false ()) prog.main_guard
+  in
+  let str = Format.flush_str_formatter () in
+  String.to_ascii str 
+
+
+module Backend = struct
+  type vc_encoding = mopsa_program 
+
+  let init_backend () = ()
+
+  type backend_context = Conditions.verification_conditions_scope
+
+  let make_context _ = assert false
+
+  let translate_expr = translate_expr
+
+  let print_encoding = print_encoding
+
+  type model = Yojson.Basic.t (* yeah, I'll have to fix that *)
+  type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
+
+  let solve_vc_encoding _ mopsa_program =
+    let prog_name =
+      "proof_obligation_"
+      ^ simplified_string_of_pos (Expr.pos mopsa_program.main_guard)
+      ^ ".u"
+    in
+    let prog_channel = open_out prog_name in
+    Printf.fprintf prog_channel "%s" (print_encoding mopsa_program);
+    close_out prog_channel;
+    Message.emit_debug "Generated new Mopsa program at %s" prog_name;
+    let process_mopsas_json j =
+      let open Yojson.Basic.Util in
+      if j |> member "success" |> to_bool then 
+        let alarms = j |> member "checks" |> to_list in
+        (* FIXME: if list.hd fails the program is safe *)
+        let toparse = List.hd alarms |> member "messages" |> to_string in
+        let pos = Str.search_forward (Str.regexp_string "Hints: ") toparse 0 in
+        let sub_until_end s from = String.sub s from (String.length s - from) in
+        let new_json_to_parse = sub_until_end toparse (pos + String.length "Hints: ") in
+        Some (Yojson.Basic.from_string new_json_to_parse)
+      else
+        let () = Message.emit_warning "Something went wrong with Mopsa: %s" (j |> member "exception" |> to_string) in None
+    in
+    let args = [|
+      "/home/raphael/work/mopsa/bin/../bin/mopsa.bin";
+      "-share-dir=/home/raphael/work/mopsa/share/mopsa";
+      "-config=universal/ymd_poly_powerint_markerset.json";
+      (* "-debug=_"; *)
+      "-max-set-size=7";
+      "-format=json";
+      "-silent";
+      "-output=tmp.json";
+      prog_name 
+    |] in
+    (* I wanted to use mopsa as a library, but we have a small issue to fix there first *)
+    (* let open Mopsa_analyzer.Framework.Runner in *)
+    (* let _ = *)
+    (*   try parse_options args analyze_files () *)
+    (*   with *)
+    (*   | Mopsa_utils.Exceptions.Panic (s, t) -> *)
+    (*     Message.emit_warning "Mopsa failed :(@.%s@%s" s t ; 0 *)
+    (*   | _ -> *)
+    (*     Message.emit_warning "Mopsa failed :("; 0 *)
+    (* in *)
+    let () = Unix.unlink "tmp.json" in
+    let _ = Unix.system (Array.fold_left (fun acc s -> acc ^ " " ^ s) "" args) in
+    match process_mopsas_json (Yojson.Basic.from_file "tmp.json") with
+    | Some hints ->
+      ProvenFalse (Some hints)
+    | None ->
+      Unknown 
+
+  let print_model _ m : string =
+    Yojson.Basic.pretty_to_string ~std:true m
+
+  let init_backend () =
+    Message.emit_debug "Running Mopsa"
+
+  let is_model_empty _ = assert false
+  let encode_asserts _ _ = assert false 
+end
+
+module Io = Io.MakeBackendIO (Backend)
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index dd00322b8..8108fa98f 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -17,253 +17,6 @@
 open Catala_utils
 open Shared_ast
 
-let simplified_string_of_pos pos =
-  let basename =
-    Filename.basename (Pos.get_file pos) |> Filename.chop_extension
-  in
-  Format.asprintf "%s_%d-%d_%d-%d" basename (Pos.get_start_line pos)
-    (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
-
-let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
-    typed Dcalc.Ast.expr Var.Set.t =
-  (* We search recursively in the possible definitions of each free variable. *)
-  let free_vars = Expr.free_vars e in
-  let possible_values_of_free_vars =
-    Var.Map.filter
-      (fun v _ -> Var.Set.mem v free_vars)
-      vc_scope_ctx.Conditions.vc_scope_possible_variable_values
-  in
-  Var.Map.fold
-    (fun _ possible_values vars_used ->
-      List.fold_left
-        (fun vars_used possible_value ->
-          Var.Set.union (vars_used_in_vc vc_scope_ctx possible_value) vars_used)
-        vars_used possible_values)
-    possible_values_of_free_vars free_vars
-
-module TypedValuesDcalcVarMap = struct
-  type 'x t = (typed Dcalc.Ast.expr, ('x, typed) marked option) Var.Map.t
-
-  let map (f : 'a -> 'b) (m : 'a t) : 'b t =
-    Var.Map.map (Option.map (fun (x, tx) -> f x, tx)) m
-end
-
-module TypedValuesDcalcVarMapBoxLifting = Bindlib.Lift (TypedValuesDcalcVarMap)
-
-type mopsa_program = {
-  main_guard : typed Dcalc.Ast.expr;
-  declared_variables :
-    ((dcalc, typed) gexpr Var.t * typed Dcalc.Ast.expr option) list;
-      (* ((typed Dcalc.Ast.expr * (typed Dcalc.Ast.expr) option)) list; *)
-}
-
-(* The goal of this part is to extract additions from expressions, and perform
-   them before as assignments. This will simplify the analysis and communication
-   with Mopsa. *)
-let turn_vc_into_mopsa_compatible_program
-    (vc : Conditions.verification_condition)
-    (vc_scope_ctx : Conditions.verification_conditions_scope) :
-    mopsa_program * Conditions.verification_conditions_scope =
-  let vars_used_in_vc = vars_used_in_vc vc_scope_ctx vc.vc_guard in
-  let vars_used_in_vc_with_known_values =
-    Var.Set.filter
-      (fun v ->
-        Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
-      vars_used_in_vc
-  in
-  let vars_used_in_vc_defined_outside_of_scope =
-    Var.Set.inter
-      vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope
-      vars_used_in_vc
-  in
-  let decls_to_top =
-    let others =
-      Var.Set.diff vars_used_in_vc
-        (Var.Set.union vars_used_in_vc_defined_outside_of_scope
-           vars_used_in_vc_with_known_values)
-    in
-    List.fold_left
-      (fun decls v -> (v, None) :: decls)
-      []
-      (Var.Set.elements
-         (Var.Set.union vars_used_in_vc_defined_outside_of_scope others))
-  in
-  let assignments =
-    List.fold_left
-      (fun decls (var, values) ->
-        if Var.Set.mem var vars_used_in_vc_with_known_values then
-          (* FIXME handle multiple values *)
-          let () = assert (List.length values = 1) in
-          (var, Some (List.hd values)) :: decls
-        else decls)
-      []
-      (Var.Map.bindings vc_scope_ctx.vc_scope_possible_variable_values)
-  in
-  let declared_variables = decls_to_top @ assignments in
-  let rec transform_field_accesses_into_variables e =
-    match Mark.remove e with
-    | EStructAccess { e = EVar v, _; _ }
-      when List.exists (fun (v2, _) -> Var.compare v v2 = 0) declared_variables
-      ->
-      let var = Var.make (Format.asprintf "%a" (Print.expr ()) e) in
-      Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
-    | _ ->
-      Expr.map_gather ~acc:Var.Map.empty
-        ~join:(Var.Map.union (fun _ _ _ -> assert false))
-        ~f:transform_field_accesses_into_variables e
-  in
-  let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
-      (typed Dcalc.Ast.expr, (dcalc, typed) boxed_gexpr option) Var.Map.t
-      * (dcalc, typed) boxed_gexpr =
-    match Mark.remove e with
-    | EApp
-        {
-          f =
-            ( EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound; tys = _ },
-              _ ) as f;
-          args;
-        } ->
-      let acc, args =
-        List.fold_left_map
-          (fun acc arg ->
-            let toadd, arg = split_expression_into_atomic_parts arg in
-            (Var.Map.union (fun _ _ _ -> assert false)) acc toadd, arg)
-          Var.Map.empty args
-      in
-      let dummy_var =
-        let pos = Expr.pos e in
-        Var.make ("var_" ^ simplified_string_of_pos pos)
-      in
-      let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
-      Var.Map.add dummy_var (Some new_e) acc, Expr.evar dummy_var (Mark.get e)
-    | _ ->
-      Expr.map_gather ~acc:Var.Map.empty
-        ~join:(Var.Map.union (fun _ _ _ -> assert false))
-        ~f:split_expression_into_atomic_parts e
-  in
-  let new_vars_fields, (e, e_mark) =
-    transform_field_accesses_into_variables vc.vc_guard
-  in
-  let new_vars_fields, vc_scope_ctx =
-    ( Var.Map.map (fun _ -> None) new_vars_fields,
-      {
-        vc_scope_ctx with
-        vc_scope_variables_typs =
-          Var.Map.union
-            (fun _ _ _ -> assert false)
-            vc_scope_ctx.vc_scope_variables_typs new_vars_fields;
-      } )
-  in
-  let new_vars_fields, e =
-    Bindlib.unbox
-      (Bindlib.box_apply2
-         (fun new_vars e -> new_vars, (e, e_mark))
-         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars_fields)
-         e)
-  in
-  let new_vars, (simple_guard, simple_guard_mark) =
-    split_expression_into_atomic_parts e
-  in
-  let new_vars, simple_guard =
-    (* This manipulation is done so that we only unbox once to keep all
-       variables in sync. *)
-    Bindlib.unbox
-      (Bindlib.box_apply2
-         (fun new_vars simple_guard ->
-           new_vars, (simple_guard, simple_guard_mark))
-         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars)
-         simple_guard)
-  in
-  ( {
-      main_guard = simple_guard;
-      declared_variables =
-        declared_variables
-        @ Var.Map.bindings new_vars_fields
-        @ List.rev
-        @@ Var.Map.bindings new_vars;
-    },
-    vc_scope_ctx )
-
-(** This function is temporarily here but should be moved to a MOPSA backend. *)
-let solve_date_vc
-    (decl_ctx : decl_ctx)
-    (scope_name : ScopeName.t)
-    (vc_scope_ctx : Conditions.verification_conditions_scope)
-    (vc : Conditions.verification_condition) =
-  Message.emit_debug "%s"
-    (Z3backend.Io.print_negative_result vc scope_name
-       (Z3backend.Io.make_context decl_ctx)
-       None);
-  let prog, vc_scope_ctx =
-    turn_vc_into_mopsa_compatible_program vc vc_scope_ctx
-  in
-  let prog_name =
-    "proof_obligation_"
-    ^ simplified_string_of_pos (Expr.pos prog.main_guard)
-    ^ ".u"
-  in
-  let prog_channel = open_out prog_name in
-  let fmt = Format.formatter_of_out_channel prog_channel in
-  let () = Format.pp_set_margin fmt 2000 in
-  let () =
-    Format.fprintf fmt "%aassert(sync(%s));@."
-      (Format.pp_print_list
-         ~pp_sep:(fun _ () -> ())
-         (fun fmt (var, oexpr) ->
-           match oexpr with
-           | None -> (
-             let ty =
-               match
-                 Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs
-               with
-               | None ->
-                 (* FIXME: I may have added to many variables in
-                    vc_scope_variables_typs in commit b08841e7, the good way to
-                    do it would be to extract types of variables from the
-                    expression directly *)
-                 let rec find_type_of_var v e =
-                   match e with
-                   | EVar v', mark when Var.compare v v' = 0 -> [mark]
-                   | e ->
-                     Expr.shallow_fold
-                       (fun e acc -> find_type_of_var v e @ acc)
-                       e []
-                 in
-                 let m = find_type_of_var var vc.vc_guard in
-                 let (Typed { ty; _ }) = List.hd m in
-                 ty
-               | Some ty -> ty
-             in
-             let make_random =
-               match Mark.remove ty with
-               | TLit TDate -> Some "date()"
-               | TLit TDuration -> Some "duration_ym()"
-               | TLit TBool -> Some "bool()"
-               | TLit TInt -> Some "int()"
-               | _ -> None
-             in
-             match make_random with
-             | Some make_random ->
-               Format.fprintf fmt "%a %s = make_random_%s;@."
-                 (Print.typ decl_ctx) ty
-                 (String.to_ascii @@ Format.asprintf "%a" Print.var var)
-                 make_random
-             | None ->
-               Message.emit_warning "Ignoring type declaration of var %a : %a"
-                 Print.var_debug var Print.typ_debug ty)
-           | Some expr ->
-             Format.fprintf fmt "%a %s = %s;@." (Print.typ decl_ctx)
-               (Expr.ty expr)
-               (String.to_ascii @@ Format.asprintf "%a" Print.var var)
-               (String.to_ascii
-               @@ Format.asprintf "%a" (Print.expr ~debug:false ()) expr)))
-      prog.declared_variables
-      (String.to_ascii
-      @@ Format.asprintf "%a" (Print.expr ~debug:false ()) prog.main_guard)
-  in
-  close_out prog_channel;
-  Message.emit_debug "Generated new Mopsa program at %s" prog_name
-
 (** [solve_vc] is the main entry point of this module. It takes a list of
     expressions [vcs] corresponding to verification conditions that must be
     discharged by Z3, and attempts to solve them **)
@@ -273,47 +26,52 @@ let solve_vcs
   (* Right now we only use the Z3 backend but the functorial interface should
      make it easy to mix and match different proof backends. *)
   Z3backend.Io.init_backend ();
+  Mopsabackend.Io.init_backend ();
   let all_proven =
     ScopeName.Map.fold
       (fun scope_name scope_vcs all_proven ->
-        let dates_vc =
-          List.filter
-            (fun vc ->
-              match vc.Conditions.vc_kind with
-              | Conditions.DateComputation -> true
-              | _ -> false)
-            scope_vcs.Conditions.vc_scope_list
-        in
-        List.iter (solve_date_vc decl_ctx scope_name scope_vcs) dates_vc;
-        let z3_vcs =
-          List.map
-            (fun vc ->
-              ( vc,
-                try
-                  let ctx = Z3backend.Io.make_context decl_ctx in
-                  let ctx =
-                    Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
-                  in
-                  let ctx, z3_vc =
-                    Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
-                  in
-                  Z3backend.Io.Success (z3_vc, ctx)
-                with Failure msg -> Fail msg ))
-            (List.filter
-               (fun vc ->
-                 match vc.Conditions.vc_kind with
-                 | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
-                   ->
-                   true
-                 | Conditions.DateComputation -> false)
-               scope_vcs.Conditions.vc_scope_list)
-        in
-        List.fold_left
-          (fun all_proven vc ->
-            if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
-              all_proven
-            else false)
-          all_proven z3_vcs)
+         let dates_vcs =
+           List.filter
+             (fun vc ->
+                match vc.Conditions.vc_kind with
+                | Conditions.DateComputation -> true
+                | _ -> false)
+             scope_vcs.Conditions.vc_scope_list |>
+           List.map (fun vc ->
+               let ctx, prog = Mopsabackend.Io.translate_expr scope_vcs vc.Conditions.vc_guard in
+               vc, Mopsabackend.Io.Success (prog, ctx)
+             ) in
+         let all_proven = List.fold_left (fun all_proven vc ->
+             if Mopsabackend.Io.check_vc decl_ctx scope_name scope_vcs vc then all_proven else false) all_proven dates_vcs in
+         let z3_vcs =
+           List.map
+             (fun vc ->
+                ( vc,
+                  try
+                    let ctx = Z3backend.Io.make_context decl_ctx in
+                    let ctx =
+                      Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
+                    in
+                    let ctx, z3_vc =
+                      Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
+                    in
+                    Z3backend.Io.Success (z3_vc, ctx)
+                  with Failure msg -> Fail msg ))
+             (List.filter
+                (fun vc ->
+                   match vc.Conditions.vc_kind with
+                   | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
+                     ->
+                     true
+                   | Conditions.DateComputation -> false)
+                scope_vcs.Conditions.vc_scope_list)
+         in
+         List.fold_left
+           (fun all_proven vc ->
+              if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
+                all_proven
+              else false)
+           all_proven z3_vcs)
       vcs true
   in
   if all_proven then

From 66678e653d21b557393df77f05223529b2ed433a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Sun, 25 Jun 2023 23:31:08 +0200
Subject: [PATCH 20/31] Mopsa backend should work (when Mopsa is installed...)

---
 compiler/verification/io.ml                | 10 ++--
 compiler/verification/io.mli               |  2 +-
 compiler/verification/mopsabackend.real.ml | 55 +++++++++++-----------
 compiler/verification/z3backend.real.ml    |  3 +-
 4 files changed, 37 insertions(+), 33 deletions(-)

diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index 2cb2768ab..b4ff53539 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -27,7 +27,7 @@ module type Backend = sig
 
   type vc_encoding
 
-  val print_encoding : vc_encoding -> string
+  val print_encoding : backend_context -> vc_encoding -> string
 
   type model
   type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
@@ -161,6 +161,7 @@ module MakeBackendIO (B : Backend) = struct
 
     Message.emit_debug "@[<v>For this variable:@,%a@,@]" Pos.format_loc_text
       (Expr.pos vc.Conditions.vc_guard);
+    if vc.vc_kind <> DateComputation then 
     Message.emit_debug
       "@[<v>This verification condition was generated for @{<yellow>%s@}:@,\
        %a@,\
@@ -190,14 +191,17 @@ module MakeBackendIO (B : Backend) = struct
     match z3_vc with
     | Success (encoding, backend_ctx) -> (
       Message.emit_debug "@[<v>The translation to Z3 is the following:@,%s@]"
-        (B.print_encoding encoding);
+        (B.print_encoding backend_ctx encoding);
       match B.solve_vc_encoding backend_ctx encoding with
       | ProvenTrue -> true
       | ProvenFalse model ->
         Message.emit_warning "%s"
           (print_negative_result vc scope backend_ctx model);
         false
-      | Unknown -> failwith "The solver failed at proving or disproving the VC")
+      | Unknown ->
+        (* FIXME: we probably want to have the choice of behavior between failure and warning here *)
+        Message.emit_warning "The solver failed at proving or disproving the VC";
+        false )
     | Fail msg ->
       Message.emit_warning
         "@[<v>@{<yellow>[%a.%s]@} The translation to Z3 failed:@,%s@]"
diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli
index a9b9559bf..6a232b0bb 100644
--- a/compiler/verification/io.mli
+++ b/compiler/verification/io.mli
@@ -28,7 +28,7 @@ module type Backend = sig
 
   type vc_encoding
 
-  val print_encoding : vc_encoding -> string
+  val print_encoding : backend_context -> vc_encoding -> string
 
   type model
   type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index 7c2fe4c51..7f54864dd 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -18,6 +18,7 @@ open Catala_utils
 open Shared_ast
 
 type mopsa_program = {
+  initial_guard : typed Dcalc.Ast.expr;
   main_guard : typed Dcalc.Ast.expr;
   declared_variables :
     ((dcalc, typed) gexpr Var.t * typed Dcalc.Ast.expr option) list;
@@ -174,6 +175,7 @@ let translate_expr vc_scope_ctx vc_guard =
   in
   (vc_scope_ctx,
    {
+     initial_guard = vc_guard;
       main_guard = simple_guard;
       declared_variables =
         declared_variables
@@ -184,7 +186,7 @@ let translate_expr vc_scope_ctx vc_guard =
 
 
 
-let print_encoding (prog : mopsa_program) =
+let print_encoding (vc_scope_ctx : Conditions.verification_conditions_scope) (prog : mopsa_program) =
   let fmt = Format.str_formatter in
   let () =
     Format.fprintf fmt "%aassert(sync(%a));@."
@@ -193,29 +195,26 @@ let print_encoding (prog : mopsa_program) =
          (fun fmt (var, oexpr) ->
            match oexpr with
            | None -> (
-             let ty =
-               let rec find_type_of_var v e =
-                 match e with
-                 | EVar v', mark when Var.compare v v' = 0 -> [mark]
-                 | e ->
-                   Expr.shallow_fold
-                     (fun e acc -> find_type_of_var v e @ acc)
-                     e []
-               in
-               let m = find_type_of_var var prog.main_guard in 
-               let (Typed { ty; _ }) = List.hd m in
-               ty in
-             (*     match *)
-             (*     Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs *)
-             (*   with *)
-             (*   | None -> *)
-             (*     (\* FIXME: I may have added to many variables in *)
-             (*        vc_scope_variables_typs in commit b08841e7, the good way to *)
-             (*        do it would be to extract types of variables from the *)
-             (*        expression directly *\) *)
-             (*   | Some ty -> ty *)
-             (* in *)
-             let make_random =
+               let ty = match Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs with
+                 | None ->
+                   (* FIXME: I may have added to many variables in
+                        vc_scope_variables_typs in commit b08841e7, the good way to
+                        do it would be to extract types of variables from the
+                        expression directly *)
+                   let rec find_type_of_var v e =
+                     match e with
+                     | EVar v', mark when Var.compare v v' = 0 -> [mark]
+                     | e ->
+                       Expr.shallow_fold
+                         (fun e acc -> find_type_of_var v e @ acc)
+                         e []
+                   in
+                   let m = find_type_of_var var prog.initial_guard in
+                   (* let () = Message.emit_debug "searching for %a in %a" Print.var_debug var (Print.expr ()) prog.initial_guard in *)
+                   let (Typed { ty; _ }) = List.hd m in
+                   ty
+                 | Some ty -> ty in
+               let make_random =
                match Mark.remove ty with
                | TLit TDate -> Some "date()"
                | TLit TDuration -> Some "duration_ym()"
@@ -255,19 +254,19 @@ module Backend = struct
 
   let translate_expr = translate_expr
 
-  let print_encoding = print_encoding
+  let print_encoding ctx prog = print_encoding ctx prog
 
   type model = Yojson.Basic.t (* yeah, I'll have to fix that *)
   type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
 
-  let solve_vc_encoding _ mopsa_program =
+  let solve_vc_encoding ctx mopsa_program =
     let prog_name =
       "proof_obligation_"
       ^ simplified_string_of_pos (Expr.pos mopsa_program.main_guard)
       ^ ".u"
     in
     let prog_channel = open_out prog_name in
-    Printf.fprintf prog_channel "%s" (print_encoding mopsa_program);
+    Printf.fprintf prog_channel "%s" (print_encoding ctx mopsa_program);
     close_out prog_channel;
     Message.emit_debug "Generated new Mopsa program at %s" prog_name;
     let process_mopsas_json j =
@@ -318,7 +317,7 @@ module Backend = struct
   let init_backend () =
     Message.emit_debug "Running Mopsa"
 
-  let is_model_empty _ = assert false
+  let is_model_empty _ = false
   let encode_asserts _ _ = assert false 
 end
 
diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index d21623bfa..d2f3bde0b 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -793,7 +793,7 @@ module Backend = struct
   type backend_context = context
   type vc_encoding = Z3.Expr.expr
 
-  let print_encoding (vc : vc_encoding) : string = Expr.to_string vc
+  let print_encoding _ (vc : vc_encoding) : string = Expr.to_string vc
 
   type model = Z3.Model.model
   type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
@@ -848,3 +848,4 @@ module Backend = struct
 end
 
 module Io = Io.MakeBackendIO (Backend)
+

From 1712de2c0e2709045ea84a3e302e54e32197f258 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Sun, 25 Jun 2023 23:31:39 +0200
Subject: [PATCH 21/31] Two temporary changes we'll have to discuss

---
 compiler/shared_ast/print.ml                                | 3 ++-
 .../code_construction_reglementaire.catala_fr               | 6 ++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml
index 08325fea4..2d56a9d74 100644
--- a/compiler/shared_ast/print.ml
+++ b/compiler/shared_ast/print.ml
@@ -542,7 +542,8 @@ let rec expr_aux :
     pr colors fmt e;
     Format.pp_close_box fmt ()
   | EApp { f = EOp { op; _ }, _; args = [arg1] } ->
-    Format.fprintf fmt "@[<hv 2>%a@ %a@]" (operator ~debug) op (rhs exprc) arg1
+    (* FIXME: I'd like to have an imperative style printing of function calls (ie f(a,b,c) rather than (f a b c)) for Mopsa export. How to concialiate both? *)
+    Format.fprintf fmt "@[<hv 2>%a(%a)@]" (operator ~debug) op (rhs exprc) arg1
   | EApp { f; args } ->
     Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f
       (Format.pp_print_list
diff --git a/examples/aides_logement/code_construction_reglementaire.catala_fr b/examples/aides_logement/code_construction_reglementaire.catala_fr
index 81f0286f4..7d8212013 100644
--- a/examples/aides_logement/code_construction_reglementaire.catala_fr
+++ b/examples/aides_logement/code_construction_reglementaire.catala_fr
@@ -2048,8 +2048,10 @@ champ d'application ÉligibilitéPrimeDeDéménagement:
       -- AprèsPremierJourMoisCivilTroisièmeMoisDeGrossesse: vrai
       -- DateDeNaissance de date_naissance:
         # VERIF: ambigü
-        date_courante <=
-          ((premier_jour_du_mois de (date_naissance + 2 an))) + (-1 jour))
+        #        date_courante <=
+        #  ((premier_jour_du_mois de (date_naissance + 2 an))) + (-1 jour))
+        date_courante < (premier_jour_du_mois de (date_naissance + 2 an))
+      )
     )
   conséquence rempli
 

From 4982679021f92cd5947cb4b2444b2cb282adeaed Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Mon, 26 Jun 2023 12:06:13 +0200
Subject: [PATCH 22/31] Formatting

---
 compiler/shared_ast/print.ml               |   4 +-
 compiler/verification/dune                 |   4 +-
 compiler/verification/io.ml                |  58 ++++----
 compiler/verification/mopsabackend.real.ml | 165 +++++++++++----------
 compiler/verification/solver.ml            |  89 ++++++-----
 compiler/verification/z3backend.real.ml    |   1 -
 6 files changed, 171 insertions(+), 150 deletions(-)

diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml
index 2d56a9d74..734dbfa48 100644
--- a/compiler/shared_ast/print.ml
+++ b/compiler/shared_ast/print.ml
@@ -542,7 +542,9 @@ let rec expr_aux :
     pr colors fmt e;
     Format.pp_close_box fmt ()
   | EApp { f = EOp { op; _ }, _; args = [arg1] } ->
-    (* FIXME: I'd like to have an imperative style printing of function calls (ie f(a,b,c) rather than (f a b c)) for Mopsa export. How to concialiate both? *)
+    (* FIXME: I'd like to have an imperative style printing of function calls
+       (ie f(a,b,c) rather than (f a b c)) for Mopsa export. How to concialiate
+       both? *)
     Format.fprintf fmt "@[<hv 2>%a(%a)@]" (operator ~debug) op (rhs exprc) arg1
   | EApp { f; args } ->
     Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f
diff --git a/compiler/verification/dune b/compiler/verification/dune
index 14fca1024..6260094b7 100644
--- a/compiler/verification/dune
+++ b/compiler/verification/dune
@@ -16,9 +16,7 @@
    mopsabackend.ml
    from
    (mopsa.mopsa_analyzer -> mopsabackend.real.ml)
-   (-> mopsabackend.dummy.ml))
- )
-)
+   (-> mopsabackend.dummy.ml))))
 
 (documentation
  (package catala)
diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index b4ff53539..3cc800e48 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -161,32 +161,33 @@ module MakeBackendIO (B : Backend) = struct
 
     Message.emit_debug "@[<v>For this variable:@,%a@,@]" Pos.format_loc_text
       (Expr.pos vc.Conditions.vc_guard);
-    if vc.vc_kind <> DateComputation then 
-    Message.emit_debug
-      "@[<v>This verification condition was generated for @{<yellow>%s@}:@,\
-       %a@,\
-       with assertions:@,\
-       %a@,\
-       and possible values for variables:@,\
-       %a@]"
-      (match vc.vc_kind with
-      | Conditions.NoEmptyError ->
-        "the variable definition never to return an empty error"
-      | NoOverlappingExceptions -> "no two exceptions to ever overlap"
-      | DateComputation -> "this date computation cannot be ambiguous")
-      (Print.expr ()) vc.vc_guard (Print.expr ()) vc_scope_ctx.vc_scope_asserts
-      (fun fmt vars_possible_values ->
-        Format.pp_print_list
-          ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
-          (fun fmt (var, values) ->
-            Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
-              (Format.pp_print_list
-                 ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
-                 (Print.expr ()))
-              values)
-          fmt
-          (Var.Map.bindings vars_possible_values))
-      vc_scope_ctx.vc_scope_possible_variable_values;
+    if vc.vc_kind <> DateComputation then
+      Message.emit_debug
+        "@[<v>This verification condition was generated for @{<yellow>%s@}:@,\
+         %a@,\
+         with assertions:@,\
+         %a@,\
+         and possible values for variables:@,\
+         %a@]"
+        (match vc.vc_kind with
+        | Conditions.NoEmptyError ->
+          "the variable definition never to return an empty error"
+        | NoOverlappingExceptions -> "no two exceptions to ever overlap"
+        | DateComputation -> "this date computation cannot be ambiguous")
+        (Print.expr ()) vc.vc_guard (Print.expr ())
+        vc_scope_ctx.vc_scope_asserts
+        (fun fmt vars_possible_values ->
+          Format.pp_print_list
+            ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
+            (fun fmt (var, values) ->
+              Format.fprintf fmt "@[<hov 2>%a@ = @ %a@]" Print.var var
+                (Format.pp_print_list
+                   ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
+                   (Print.expr ()))
+                values)
+            fmt
+            (Var.Map.bindings vars_possible_values))
+        vc_scope_ctx.vc_scope_possible_variable_values;
 
     match z3_vc with
     | Success (encoding, backend_ctx) -> (
@@ -199,9 +200,10 @@ module MakeBackendIO (B : Backend) = struct
           (print_negative_result vc scope backend_ctx model);
         false
       | Unknown ->
-        (* FIXME: we probably want to have the choice of behavior between failure and warning here *)
+        (* FIXME: we probably want to have the choice of behavior between
+           failure and warning here *)
         Message.emit_warning "The solver failed at proving or disproving the VC";
-        false )
+        false)
     | Fail msg ->
       Message.emit_warning
         "@[<v>@{<yellow>[%a.%s]@} The translation to Z3 failed:@,%s@]"
diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index 7f54864dd..58ac18533 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -1,6 +1,7 @@
 (* This file is part of the Catala compiler, a specification language for tax
-   and social benefits computation rules. Copyright (C) 2023 Inria, contributors:
-   Raphaël Monat <raphael.monat@inria.fr>, Denis Merigoux <denis.merigoux@inria.fr>
+   and social benefits computation rules. Copyright (C) 2023 Inria,
+   contributors: Raphaël Monat <raphael.monat@inria.fr>, Denis Merigoux
+   <denis.merigoux@inria.fr>
 
    Licensed under the Apache License, Version 2.0 (the "License"); you may not
    use this file except in compliance with the License. You may obtain a copy of
@@ -24,7 +25,6 @@ type mopsa_program = {
     ((dcalc, typed) gexpr Var.t * typed Dcalc.Ast.expr option) list;
 }
 
-
 let simplified_string_of_pos pos =
   let basename =
     Filename.basename (Pos.get_file pos) |> Filename.chop_extension
@@ -33,7 +33,7 @@ let simplified_string_of_pos pos =
     (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
 
 let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
-  typed Dcalc.Ast.expr Var.Set.t =
+    typed Dcalc.Ast.expr Var.Set.t =
   (* We search recursively in the possible definitions of each free variable. *)
   let free_vars = Expr.free_vars e in
   let possible_values_of_free_vars =
@@ -43,10 +43,10 @@ let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
   in
   Var.Map.fold
     (fun _ possible_values vars_used ->
-       List.fold_left
-         (fun vars_used possible_value ->
-            Var.Set.union (vars_used_in_vc vc_scope_ctx possible_value) vars_used)
-         vars_used possible_values)
+      List.fold_left
+        (fun vars_used possible_value ->
+          Var.Set.union (vars_used_in_vc vc_scope_ctx possible_value) vars_used)
+        vars_used possible_values)
     possible_values_of_free_vars free_vars
 
 module TypedValuesDcalcVarMap = struct
@@ -58,7 +58,6 @@ end
 
 module TypedValuesDcalcVarMapBoxLifting = Bindlib.Lift (TypedValuesDcalcVarMap)
 
-
 (* The goal of this part is to extract additions from expressions, and perform
    them before as assignments. This will simplify the analysis and communication
    with Mopsa. *)
@@ -118,7 +117,13 @@ let translate_expr vc_scope_ctx vc_guard =
     | EApp
         {
           f =
-            ( EOp { op = Op.Add_dat_dur Dates_calc.Dates.AbortOnRound | Op.FirstDayOfMonth; tys = _ },
+            ( EOp
+                {
+                  op =
+                    ( Op.Add_dat_dur Dates_calc.Dates.AbortOnRound
+                    | Op.FirstDayOfMonth );
+                  tys = _;
+                },
               _ ) as f;
           args;
         } ->
@@ -173,20 +178,20 @@ let translate_expr vc_scope_ctx vc_guard =
          (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars)
          simple_guard)
   in
-  (vc_scope_ctx,
-   {
-     initial_guard = vc_guard;
+  ( vc_scope_ctx,
+    {
+      initial_guard = vc_guard;
       main_guard = simple_guard;
       declared_variables =
         declared_variables
         @ Var.Map.bindings new_vars_fields
         @ List.rev
         @@ Var.Map.bindings new_vars;
-    })
-
+    } )
 
-
-let print_encoding (vc_scope_ctx : Conditions.verification_conditions_scope) (prog : mopsa_program) =
+let print_encoding
+    (vc_scope_ctx : Conditions.verification_conditions_scope)
+    (prog : mopsa_program) =
   let fmt = Format.str_formatter in
   let () =
     Format.fprintf fmt "%aassert(sync(%a));@."
@@ -195,26 +200,31 @@ let print_encoding (vc_scope_ctx : Conditions.verification_conditions_scope) (pr
          (fun fmt (var, oexpr) ->
            match oexpr with
            | None -> (
-               let ty = match Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs with
-                 | None ->
-                   (* FIXME: I may have added to many variables in
-                        vc_scope_variables_typs in commit b08841e7, the good way to
-                        do it would be to extract types of variables from the
-                        expression directly *)
-                   let rec find_type_of_var v e =
-                     match e with
-                     | EVar v', mark when Var.compare v v' = 0 -> [mark]
-                     | e ->
-                       Expr.shallow_fold
-                         (fun e acc -> find_type_of_var v e @ acc)
-                         e []
-                   in
-                   let m = find_type_of_var var prog.initial_guard in
-                   (* let () = Message.emit_debug "searching for %a in %a" Print.var_debug var (Print.expr ()) prog.initial_guard in *)
-                   let (Typed { ty; _ }) = List.hd m in
-                   ty
-                 | Some ty -> ty in
-               let make_random =
+             let ty =
+               match
+                 Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs
+               with
+               | None ->
+                 (* FIXME: I may have added to many variables in
+                    vc_scope_variables_typs in commit b08841e7, the good way to
+                    do it would be to extract types of variables from the
+                    expression directly *)
+                 let rec find_type_of_var v e =
+                   match e with
+                   | EVar v', mark when Var.compare v v' = 0 -> [mark]
+                   | e ->
+                     Expr.shallow_fold
+                       (fun e acc -> find_type_of_var v e @ acc)
+                       e []
+                 in
+                 let m = find_type_of_var var prog.initial_guard in
+                 (* let () = Message.emit_debug "searching for %a in %a"
+                    Print.var_debug var (Print.expr ()) prog.initial_guard in *)
+                 let (Typed { ty; _ }) = List.hd m in
+                 ty
+               | Some ty -> ty
+             in
+             let make_random =
                match Mark.remove ty with
                | TLit TDate -> Some "date()"
                | TLit TDuration -> Some "duration_ym()"
@@ -224,36 +234,32 @@ let print_encoding (vc_scope_ctx : Conditions.verification_conditions_scope) (pr
              in
              match make_random with
              | Some make_random ->
-               Format.fprintf fmt "%a %a = make_random_%s;@."
-                 Print.typ_debug ty
-                 Print.var var
-                 make_random
+               Format.fprintf fmt "%a %a = make_random_%s;@." Print.typ_debug ty
+                 Print.var var make_random
              | None ->
                Message.emit_warning "Ignoring type declaration of var %a : %a"
                  Print.var_debug var Print.typ_debug ty)
            | Some expr ->
-             Format.fprintf fmt "%a %a = %a;@."
-               Print.typ_debug (Expr.ty expr)
+             Format.fprintf fmt "%a %a = %a;@." Print.typ_debug (Expr.ty expr)
                Print.var var
-               (Print.expr ~debug:false ()) expr))
+               (Print.expr ~debug:false ())
+               expr))
       prog.declared_variables
-      (Print.expr ~debug:false ()) prog.main_guard
+      (Print.expr ~debug:false ())
+      prog.main_guard
   in
   let str = Format.flush_str_formatter () in
-  String.to_ascii str 
-
+  String.to_ascii str
 
 module Backend = struct
-  type vc_encoding = mopsa_program 
+  type vc_encoding = mopsa_program
 
   let init_backend () = ()
 
   type backend_context = Conditions.verification_conditions_scope
 
   let make_context _ = assert false
-
   let translate_expr = translate_expr
-
   let print_encoding ctx prog = print_encoding ctx prog
 
   type model = Yojson.Basic.t (* yeah, I'll have to fix that *)
@@ -271,29 +277,38 @@ module Backend = struct
     Message.emit_debug "Generated new Mopsa program at %s" prog_name;
     let process_mopsas_json j =
       let open Yojson.Basic.Util in
-      if j |> member "success" |> to_bool then 
+      if j |> member "success" |> to_bool then
         let alarms = j |> member "checks" |> to_list in
         (* FIXME: if list.hd fails the program is safe *)
         let toparse = List.hd alarms |> member "messages" |> to_string in
         let pos = Str.search_forward (Str.regexp_string "Hints: ") toparse 0 in
         let sub_until_end s from = String.sub s from (String.length s - from) in
-        let new_json_to_parse = sub_until_end toparse (pos + String.length "Hints: ") in
+        let new_json_to_parse =
+          sub_until_end toparse (pos + String.length "Hints: ")
+        in
         Some (Yojson.Basic.from_string new_json_to_parse)
       else
-        let () = Message.emit_warning "Something went wrong with Mopsa: %s" (j |> member "exception" |> to_string) in None
+        let () =
+          Message.emit_warning "Something went wrong with Mopsa: %s"
+            (j |> member "exception" |> to_string)
+        in
+        None
+    in
+    let args =
+      [|
+        "/home/raphael/work/mopsa/bin/../bin/mopsa.bin";
+        "-share-dir=/home/raphael/work/mopsa/share/mopsa";
+        "-config=universal/ymd_poly_powerint_markerset.json";
+        (* "-debug=_"; *)
+        "-max-set-size=7";
+        "-format=json";
+        "-silent";
+        "-output=tmp.json";
+        prog_name;
+      |]
     in
-    let args = [|
-      "/home/raphael/work/mopsa/bin/../bin/mopsa.bin";
-      "-share-dir=/home/raphael/work/mopsa/share/mopsa";
-      "-config=universal/ymd_poly_powerint_markerset.json";
-      (* "-debug=_"; *)
-      "-max-set-size=7";
-      "-format=json";
-      "-silent";
-      "-output=tmp.json";
-      prog_name 
-    |] in
-    (* I wanted to use mopsa as a library, but we have a small issue to fix there first *)
+    (* I wanted to use mopsa as a library, but we have a small issue to fix
+       there first *)
     (* let open Mopsa_analyzer.Framework.Runner in *)
     (* let _ = *)
     (*   try parse_options args analyze_files () *)
@@ -304,21 +319,17 @@ module Backend = struct
     (*     Message.emit_warning "Mopsa failed :("; 0 *)
     (* in *)
     let () = Unix.unlink "tmp.json" in
-    let _ = Unix.system (Array.fold_left (fun acc s -> acc ^ " " ^ s) "" args) in
+    let _ =
+      Unix.system (Array.fold_left (fun acc s -> acc ^ " " ^ s) "" args)
+    in
     match process_mopsas_json (Yojson.Basic.from_file "tmp.json") with
-    | Some hints ->
-      ProvenFalse (Some hints)
-    | None ->
-      Unknown 
-
-  let print_model _ m : string =
-    Yojson.Basic.pretty_to_string ~std:true m
-
-  let init_backend () =
-    Message.emit_debug "Running Mopsa"
+    | Some hints -> ProvenFalse (Some hints)
+    | None -> Unknown
 
+  let print_model _ m : string = Yojson.Basic.pretty_to_string ~std:true m
+  let init_backend () = Message.emit_debug "Running Mopsa"
   let is_model_empty _ = false
-  let encode_asserts _ _ = assert false 
+  let encode_asserts _ _ = assert false
 end
 
 module Io = Io.MakeBackendIO (Backend)
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 8108fa98f..07516d531 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -30,48 +30,57 @@ let solve_vcs
   let all_proven =
     ScopeName.Map.fold
       (fun scope_name scope_vcs all_proven ->
-         let dates_vcs =
-           List.filter
-             (fun vc ->
-                match vc.Conditions.vc_kind with
-                | Conditions.DateComputation -> true
-                | _ -> false)
-             scope_vcs.Conditions.vc_scope_list |>
-           List.map (fun vc ->
-               let ctx, prog = Mopsabackend.Io.translate_expr scope_vcs vc.Conditions.vc_guard in
-               vc, Mopsabackend.Io.Success (prog, ctx)
-             ) in
-         let all_proven = List.fold_left (fun all_proven vc ->
-             if Mopsabackend.Io.check_vc decl_ctx scope_name scope_vcs vc then all_proven else false) all_proven dates_vcs in
-         let z3_vcs =
-           List.map
-             (fun vc ->
-                ( vc,
-                  try
-                    let ctx = Z3backend.Io.make_context decl_ctx in
-                    let ctx =
-                      Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
-                    in
-                    let ctx, z3_vc =
-                      Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
-                    in
-                    Z3backend.Io.Success (z3_vc, ctx)
-                  with Failure msg -> Fail msg ))
-             (List.filter
-                (fun vc ->
-                   match vc.Conditions.vc_kind with
-                   | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
-                     ->
-                     true
-                   | Conditions.DateComputation -> false)
-                scope_vcs.Conditions.vc_scope_list)
-         in
-         List.fold_left
-           (fun all_proven vc ->
-              if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
+        let dates_vcs =
+          List.filter
+            (fun vc ->
+              match vc.Conditions.vc_kind with
+              | Conditions.DateComputation -> true
+              | _ -> false)
+            scope_vcs.Conditions.vc_scope_list
+          |> List.map (fun vc ->
+                 let ctx, prog =
+                   Mopsabackend.Io.translate_expr scope_vcs
+                     vc.Conditions.vc_guard
+                 in
+                 vc, Mopsabackend.Io.Success (prog, ctx))
+        in
+        let all_proven =
+          List.fold_left
+            (fun all_proven vc ->
+              if Mopsabackend.Io.check_vc decl_ctx scope_name scope_vcs vc then
                 all_proven
               else false)
-           all_proven z3_vcs)
+            all_proven dates_vcs
+        in
+        let z3_vcs =
+          List.map
+            (fun vc ->
+              ( vc,
+                try
+                  let ctx = Z3backend.Io.make_context decl_ctx in
+                  let ctx =
+                    Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
+                  in
+                  let ctx, z3_vc =
+                    Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
+                  in
+                  Z3backend.Io.Success (z3_vc, ctx)
+                with Failure msg -> Fail msg ))
+            (List.filter
+               (fun vc ->
+                 match vc.Conditions.vc_kind with
+                 | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
+                   ->
+                   true
+                 | Conditions.DateComputation -> false)
+               scope_vcs.Conditions.vc_scope_list)
+        in
+        List.fold_left
+          (fun all_proven vc ->
+            if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
+              all_proven
+            else false)
+          all_proven z3_vcs)
       vcs true
   in
   if all_proven then
diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index d2f3bde0b..ff6c546ff 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -848,4 +848,3 @@ module Backend = struct
 end
 
 module Io = Io.MakeBackendIO (Backend)
-

From c4b554bd5c0713366d1a09cdbf43d56b66a53538 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Mon, 26 Jun 2023 13:38:03 +0200
Subject: [PATCH 23/31] Temporary fix in verification's dune

---
 compiler/verification/dune                 |  4 ++--
 compiler/verification/mopsabackend.real.ml | 26 +++++++++++-----------
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/compiler/verification/dune b/compiler/verification/dune
index 6260094b7..60fbae4cb 100644
--- a/compiler/verification/dune
+++ b/compiler/verification/dune
@@ -2,6 +2,7 @@
  (name verification)
  (public_name catala.verification)
  (libraries
+  str
   bindlib
   catala_utils
   dcalc
@@ -15,8 +16,7 @@
   (select
    mopsabackend.ml
    from
-   (mopsa.mopsa_analyzer -> mopsabackend.real.ml)
-   (-> mopsabackend.dummy.ml))))
+   (-> mopsabackend.real.ml))))
 
 (documentation
  (package catala)
diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index 58ac18533..377fe7320 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -294,21 +294,21 @@ module Backend = struct
         in
         None
     in
-    let args =
-      [|
-        "/home/raphael/work/mopsa/bin/../bin/mopsa.bin";
-        "-share-dir=/home/raphael/work/mopsa/share/mopsa";
-        "-config=universal/ymd_poly_powerint_markerset.json";
-        (* "-debug=_"; *)
-        "-max-set-size=7";
-        "-format=json";
-        "-silent";
-        "-output=tmp.json";
-        prog_name;
-      |]
-    in
     (* I wanted to use mopsa as a library, but we have a small issue to fix
        there first *)
+    let args = [|
+      "mopsa.bin";
+      "-share-dir=/home/raphael/work/mopsa/share/mopsa";
+      "-config=universal/ymd_poly_powerint_markerset.json";
+      (* "-debug=_"; *)
+      "-max-set-size=7";
+      "-numeric=polkagrid";
+      "-format=json";
+      "-silent";
+      "-output=tmp.json";
+      prog_name 
+    |] in
+    (* I wanted to use mopsa as a library, but we have a small issue to fix there first *)
     (* let open Mopsa_analyzer.Framework.Runner in *)
     (* let _ = *)
     (*   try parse_options args analyze_files () *)

From 0ccc1d0095fee77ae2ea90a1475a6822903c6b29 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Mon, 26 Jun 2023 13:42:34 +0200
Subject: [PATCH 24/31] Unlinking unexisting files may crash indeed

---
 compiler/verification/mopsabackend.real.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index 377fe7320..77307841c 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -318,7 +318,9 @@ module Backend = struct
     (*   | _ -> *)
     (*     Message.emit_warning "Mopsa failed :("; 0 *)
     (* in *)
-    let () = Unix.unlink "tmp.json" in
+    let () =
+      try Unix.unlink "tmp.json"
+      with Unix.Unix_error _ -> () in
     let _ =
       Unix.system (Array.fold_left (fun acc s -> acc ^ " " ^ s) "" args)
     in

From 2c45eece7262efa0e5cdd4cc58f07863e1419c9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Mon, 26 Jun 2023 13:44:58 +0200
Subject: [PATCH 25/31] Call mopsa-universal to avoid share path issues

---
 compiler/verification/mopsabackend.real.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index 77307841c..66838c206 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -297,8 +297,7 @@ module Backend = struct
     (* I wanted to use mopsa as a library, but we have a small issue to fix
        there first *)
     let args = [|
-      "mopsa.bin";
-      "-share-dir=/home/raphael/work/mopsa/share/mopsa";
+      "mopsa-universal";
       "-config=universal/ymd_poly_powerint_markerset.json";
       (* "-debug=_"; *)
       "-max-set-size=7";

From ebe3efb97c21c0f5ee5c1829f05dcb1b1790dbc5 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Tue, 27 Jun 2023 10:23:04 +0200
Subject: [PATCH 26/31] Formatting

---
 compiler/verification/mopsabackend.real.ml | 33 +++++++++++-----------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index 66838c206..0ea523fef 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -237,7 +237,7 @@ let print_encoding
                Format.fprintf fmt "%a %a = make_random_%s;@." Print.typ_debug ty
                  Print.var var make_random
              | None ->
-               Message.emit_warning "Ignoring type declaration of var %a : %a"
+               Message.emit_debug "Ignoring type declaration of var %a : %a"
                  Print.var_debug var Print.typ_debug ty)
            | Some expr ->
              Format.fprintf fmt "%a %a = %a;@." Print.typ_debug (Expr.ty expr)
@@ -296,18 +296,21 @@ module Backend = struct
     in
     (* I wanted to use mopsa as a library, but we have a small issue to fix
        there first *)
-    let args = [|
-      "mopsa-universal";
-      "-config=universal/ymd_poly_powerint_markerset.json";
-      (* "-debug=_"; *)
-      "-max-set-size=7";
-      "-numeric=polkagrid";
-      "-format=json";
-      "-silent";
-      "-output=tmp.json";
-      prog_name 
-    |] in
-    (* I wanted to use mopsa as a library, but we have a small issue to fix there first *)
+    let args =
+      [|
+        "mopsa-universal";
+        "-config=universal/ymd_poly_powerint_markerset.json";
+        (* "-debug=_"; *)
+        "-max-set-size=7";
+        "-numeric=polkagrid";
+        "-format=json";
+        "-silent";
+        "-output=tmp.json";
+        prog_name;
+      |]
+    in
+    (* I wanted to use mopsa as a library, but we have a small issue to fix
+       there first *)
     (* let open Mopsa_analyzer.Framework.Runner in *)
     (* let _ = *)
     (*   try parse_options args analyze_files () *)
@@ -317,9 +320,7 @@ module Backend = struct
     (*   | _ -> *)
     (*     Message.emit_warning "Mopsa failed :("; 0 *)
     (* in *)
-    let () =
-      try Unix.unlink "tmp.json"
-      with Unix.Unix_error _ -> () in
+    let () = try Unix.unlink "tmp.json" with Unix.Unix_error _ -> () in
     let _ =
       Unix.system (Array.fold_left (fun acc s -> acc ^ " " ^ s) "" args)
     in

From 5a88ad8eba47a1c7faaf66ad0416ca2b41fbbf40 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Tue, 27 Jun 2023 14:00:44 +0200
Subject: [PATCH 27/31] Cleaner code and more robust MOPSA obligation
 infrastructure

---
 compiler/shared_ast/var.ml                 |   3 +
 compiler/shared_ast/var.mli                |   3 +
 compiler/verification/mopsabackend.real.ml | 255 +++++++++++++--------
 compiler/verification/solver.ml            |  42 ++--
 4 files changed, 177 insertions(+), 126 deletions(-)

diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index 738e633ae..605185565 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -80,6 +80,7 @@ module Set = struct
   let filter f s = filter (fun v -> f (get v)) s
   let exists f s = exists (fun v -> f (get v)) s
   let inter s1 s2 = inter s1 s2
+  let fold f s init = fold (fun v acc -> f (get v) acc) s init
 
   (* Add more as needed *)
 end
@@ -100,10 +101,12 @@ module Map = struct
   let find_opt v m = find_opt (t v) m
   let bindings m = bindings m |> List.map (fun (v, x) -> get v, x)
   let map f m = map f m
+  let mapi f m = mapi (fun v x -> f (get v) x) m
   let mem x m = mem (t x) m
   let union f m1 m2 = union (fun v x1 x2 -> f (get v) x1 x2) m1 m2
   let fold f m acc = fold (fun v x acc -> f (get v) x acc) m acc
   let filter f m = filter (fun k v -> f (get k) v) m
+  let exists f m = exists (fun k v -> f (get k) v) m
 
   (* Add more as needed *)
 end
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index 20628f5c3..a3b69a2c8 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -53,6 +53,7 @@ module Set : sig
   val filter : ('e var -> bool) -> 'e t -> 'e t
   val exists : ('e var -> bool) -> 'e t -> bool
   val inter : 'e t -> 'e t -> 'e t
+  val fold : ('e var -> 'x -> 'x) -> 'e t -> 'x -> 'x
 end
 
 (** Wrapper over [Map.S] but with a type variable for the AST type parameters.
@@ -69,10 +70,12 @@ module Map : sig
   val bindings : ('e, 'x) t -> ('e var * 'x) list
   val mem : 'e var -> ('e, 'x) t -> bool
   val map : ('x -> 'y) -> ('e, 'x) t -> ('e, 'y) t
+  val mapi : ('e var -> 'x -> 'y) -> ('e, 'x) t -> ('e, 'y) t
   val filter : ('e var -> 'x -> bool) -> ('e, 'x) t -> ('e, 'x) t
 
   val union :
     ('e var -> 'x -> 'x -> 'x option) -> ('e, 'x) t -> ('e, 'x) t -> ('e, 'x) t
 
   val fold : ('e var -> 'x -> 'acc -> 'acc) -> ('e, 'x) t -> 'acc -> 'acc
+  val exists : ('e var -> 'x -> bool) -> ('e, 'x) t -> bool
 end
diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index 0ea523fef..16b4ff640 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -58,135 +58,196 @@ end
 
 module TypedValuesDcalcVarMapBoxLifting = Bindlib.Lift (TypedValuesDcalcVarMap)
 
+(** Sometimes VC contains struct accesses from larger values which are defined
+    elsewhere. Since MOPSA does not currently handle structs, etc., we prefer
+    replacing the struct access with its own variable coming with an unknown
+    value. *)
+let rec transform_field_accesses_into_variables
+    ~(is_vc_var : (dcalc, typed) naked_gexpr Bindlib.var -> bool)
+    (e : typed Dcalc.Ast.expr) :
+    (typed Dcalc.Ast.expr, typ) Var.Map.t * (dcalc, typed) boxed_gexpr =
+  match Mark.remove e with
+  | EStructAccess { e = EVar v, _; field; _ } when is_vc_var v ->
+    let var =
+      Var.make (Format.asprintf "%a__%a" Print.var v StructField.format_t field)
+    in
+    Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
+  | _ ->
+    Expr.map_gather ~acc:Var.Map.empty
+      ~join:(Var.Map.union (fun _ _ _ -> assert false))
+      ~f:(transform_field_accesses_into_variables ~is_vc_var)
+      e
+
+type mopsa_variable_declarations =
+  (typed Dcalc.Ast.expr, (dcalc, typed) gexpr option) Var.Map.t
+
+type mopsa_variable_boxed_declarations =
+  (typed Dcalc.Ast.expr, (dcalc, typed) boxed_gexpr option) Var.Map.t
+
+module VarVertex = struct
+  include Var
+
+  type t = typed Dcalc.Ast.expr Var.t
+
+  let hash x = Bindlib.uid_of x
+  let equal x y = Bindlib.eq_vars x y
+end
+
+module VarDependencies =
+  Graph.Persistent.Digraph.ConcreteBidirectional (VarVertex)
+
+module VarDependenciesTraversal = Graph.Topological.Make (VarDependencies)
+
+let declaration_reverse_dependency_ordering (d : mopsa_variable_declarations) :
+    typed Dcalc.Ast.expr Var.t list =
+  let g = VarDependencies.empty in
+  let g =
+    Var.Map.fold
+      (fun (v : typed Dcalc.Ast.expr Var.t) (e : typed Dcalc.Ast.expr option) g ->
+        let g = VarDependencies.add_vertex g v in
+        match e with
+        | None -> g
+        | Some e ->
+          let used = Expr.free_vars e in
+          Var.Set.fold (fun used g -> VarDependencies.add_edge g used v) used g)
+      d g
+  in
+  List.rev (VarDependenciesTraversal.fold (fun v acc -> v :: acc) g [])
+
+(** To better split the load for MOPSA and improve debugging, we split the VC
+    into smaller parts by creating supplementary variables. *)
+let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
+    mopsa_variable_boxed_declarations * (dcalc, typed) boxed_gexpr =
+  match Mark.remove e with
+  | EApp
+      {
+        f =
+          ( EOp
+              {
+                op =
+                  ( Op.Add_dat_dur Dates_calc.Dates.AbortOnRound
+                  | Op.FirstDayOfMonth );
+                tys = _;
+              },
+            _ ) as f;
+        args;
+      } ->
+    let acc, args =
+      List.fold_left_map
+        (fun acc arg ->
+          let toadd, arg = split_expression_into_atomic_parts arg in
+          (Var.Map.union (fun _ _ _ -> assert false)) acc toadd, arg)
+        Var.Map.empty args
+    in
+    let dummy_var =
+      let pos = Expr.pos e in
+      Var.make ("var_" ^ simplified_string_of_pos pos)
+    in
+    let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
+    Var.Map.add dummy_var (Some new_e) acc, Expr.evar dummy_var (Mark.get e)
+  | _ ->
+    Expr.map_gather ~acc:Var.Map.empty
+      ~join:(Var.Map.union (fun _ _ _ -> assert false))
+      ~f:split_expression_into_atomic_parts e
+
 (* The goal of this part is to extract additions from expressions, and perform
    them before as assignments. This will simplify the analysis and communication
    with Mopsa. *)
-let translate_expr vc_scope_ctx vc_guard =
-  let vars_used_in_vc = vars_used_in_vc vc_scope_ctx vc_guard in
+let translate_expr
+    (vc_scope_ctx : Conditions.verification_conditions_scope)
+    (original_vc_guard : typed Dcalc.Ast.expr) =
+  let vars_used_in_vc = vars_used_in_vc vc_scope_ctx original_vc_guard in
   let vars_used_in_vc_with_known_values =
     Var.Set.filter
       (fun v ->
         Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
       vars_used_in_vc
   in
-  let vars_used_in_vc_defined_outside_of_scope =
-    Var.Set.inter
-      vc_scope_ctx.Conditions.vc_scope_variables_defined_outside_of_scope
-      vars_used_in_vc
+  let vc_variables_declarations_unknown =
+    Var.Set.fold
+      (fun v declarations -> Var.Map.add v None declarations)
+      (Var.Set.diff vars_used_in_vc vars_used_in_vc_with_known_values)
+      Var.Map.empty
   in
-  let decls_to_top =
-    let others =
-      Var.Set.diff vars_used_in_vc
-        (Var.Set.union vars_used_in_vc_defined_outside_of_scope
-           vars_used_in_vc_with_known_values)
-    in
-    List.fold_left
-      (fun decls v -> (v, None) :: decls)
-      []
-      (Var.Set.elements
-         (Var.Set.union vars_used_in_vc_defined_outside_of_scope others))
-  in
-  let assignments =
-    List.fold_left
-      (fun decls (var, values) ->
-        if Var.Set.mem var vars_used_in_vc_with_known_values then
-          (* FIXME handle multiple values *)
-          let () = assert (List.length values = 1) in
-          (var, Some (List.hd values)) :: decls
-        else decls)
-      []
-      (Var.Map.bindings vc_scope_ctx.vc_scope_possible_variable_values)
-  in
-  let declared_variables = decls_to_top @ assignments in
-  let rec transform_field_accesses_into_variables e =
-    match Mark.remove e with
-    | EStructAccess { e = EVar v, _; _ }
-      when List.exists (fun (v2, _) -> Var.compare v v2 = 0) declared_variables
-      ->
-      let var = Var.make (Format.asprintf "%a" (Print.expr ()) e) in
-      Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
-    | _ ->
-      Expr.map_gather ~acc:Var.Map.empty
-        ~join:(Var.Map.union (fun _ _ _ -> assert false))
-        ~f:transform_field_accesses_into_variables e
+  let vc_variables_declarations_defined =
+    Var.Map.mapi
+      (fun var values ->
+        if List.length values <> 1 then
+          Message.emit_debug
+            "Only the first possible value was taken into account for %a"
+            Print.var_debug var;
+        (* FIXME: take into account multiple possible values *)
+        Some (List.hd values))
+      (Var.Map.filter
+         (fun v _ -> Var.Set.mem v vars_used_in_vc)
+         vc_scope_ctx.vc_scope_possible_variable_values)
   in
-  let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
-      (typed Dcalc.Ast.expr, (dcalc, typed) boxed_gexpr option) Var.Map.t
-      * (dcalc, typed) boxed_gexpr =
-    match Mark.remove e with
-    | EApp
-        {
-          f =
-            ( EOp
-                {
-                  op =
-                    ( Op.Add_dat_dur Dates_calc.Dates.AbortOnRound
-                    | Op.FirstDayOfMonth );
-                  tys = _;
-                },
-              _ ) as f;
-          args;
-        } ->
-      let acc, args =
-        List.fold_left_map
-          (fun acc arg ->
-            let toadd, arg = split_expression_into_atomic_parts arg in
-            (Var.Map.union (fun _ _ _ -> assert false)) acc toadd, arg)
-          Var.Map.empty args
-      in
-      let dummy_var =
-        let pos = Expr.pos e in
-        Var.make ("var_" ^ simplified_string_of_pos pos)
-      in
-      let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
-      Var.Map.add dummy_var (Some new_e) acc, Expr.evar dummy_var (Mark.get e)
-    | _ ->
-      Expr.map_gather ~acc:Var.Map.empty
-        ~join:(Var.Map.union (fun _ _ _ -> assert false))
-        ~f:split_expression_into_atomic_parts e
+  let vc_variables_declarations =
+    Var.Map.union
+      (fun _ _ -> assert false)
+      vc_variables_declarations_unknown vc_variables_declarations_defined
   in
-  let new_vars_fields, (e, e_mark) =
-    transform_field_accesses_into_variables vc_guard
+  let new_vars_for_struct_accesses, (vc_guard, vc_guard_mark) =
+    transform_field_accesses_into_variables
+      ~is_vc_var:(fun v ->
+        Var.Map.exists
+          (fun v2 _ -> Var.compare v v2 = 0)
+          vc_variables_declarations)
+      original_vc_guard
   in
-  let new_vars_fields, vc_scope_ctx =
-    ( Var.Map.map (fun _ -> None) new_vars_fields,
+  let new_vars_for_struct_accesses, vc_scope_ctx =
+    ( Var.Map.map (fun _ -> None) new_vars_for_struct_accesses,
       {
         vc_scope_ctx with
         vc_scope_variables_typs =
           Var.Map.union
             (fun _ _ _ -> assert false)
-            vc_scope_ctx.vc_scope_variables_typs new_vars_fields;
+            vc_scope_ctx.vc_scope_variables_typs new_vars_for_struct_accesses;
       } )
   in
-  let new_vars_fields, e =
+  let new_vars_for_struct_accesses, vc_guard =
     Bindlib.unbox
       (Bindlib.box_apply2
-         (fun new_vars e -> new_vars, (e, e_mark))
-         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars_fields)
-         e)
+         (fun new_vars_for_struct_accesses vc_guard ->
+           new_vars_for_struct_accesses, (vc_guard, vc_guard_mark))
+         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars_for_struct_accesses)
+         vc_guard)
   in
-  let new_vars, (simple_guard, simple_guard_mark) =
-    split_expression_into_atomic_parts e
+  let new_vars_for_atomic_splitting, (vc_guard, vc_guard_mark) =
+    split_expression_into_atomic_parts vc_guard
   in
-  let new_vars, simple_guard =
+  let new_vars_for_atomic_splitting, vc_guard =
     (* This manipulation is done so that we only unbox once to keep all
        variables in sync. *)
     Bindlib.unbox
       (Bindlib.box_apply2
-         (fun new_vars simple_guard ->
-           new_vars, (simple_guard, simple_guard_mark))
-         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars)
-         simple_guard)
+         (fun new_vars_for_atomic_splitting vc_guard ->
+           new_vars_for_atomic_splitting, (vc_guard, vc_guard_mark))
+         (TypedValuesDcalcVarMapBoxLifting.lift_box
+            new_vars_for_atomic_splitting)
+         vc_guard)
+  in
+  let vc_variables_declarations =
+    Var.Map.union
+      (fun _ _ -> assert false)
+      vc_variables_declarations
+      (Var.Map.union
+         (fun _ _ -> assert false)
+         new_vars_for_struct_accesses new_vars_for_atomic_splitting)
+  in
+  let declaration_reverse_dependency_ordering =
+    declaration_reverse_dependency_ordering vc_variables_declarations
   in
   ( vc_scope_ctx,
     {
-      initial_guard = vc_guard;
-      main_guard = simple_guard;
+      initial_guard = original_vc_guard;
+      main_guard = vc_guard;
       declared_variables =
-        declared_variables
-        @ Var.Map.bindings new_vars_fields
-        @ List.rev
-        @@ Var.Map.bindings new_vars;
+        (* Careful with the order! these definitions must be laid out in reverse
+           dependency order *)
+        List.map
+          (fun v -> v, Var.Map.find v vc_variables_declarations)
+          declaration_reverse_dependency_ordering;
     } )
 
 let print_encoding
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index 07516d531..bd4985993 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -52,35 +52,19 @@ let solve_vcs
               else false)
             all_proven dates_vcs
         in
-        let z3_vcs =
-          List.map
-            (fun vc ->
-              ( vc,
-                try
-                  let ctx = Z3backend.Io.make_context decl_ctx in
-                  let ctx =
-                    Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts
-                  in
-                  let ctx, z3_vc =
-                    Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
-                  in
-                  Z3backend.Io.Success (z3_vc, ctx)
-                with Failure msg -> Fail msg ))
-            (List.filter
-               (fun vc ->
-                 match vc.Conditions.vc_kind with
-                 | Conditions.NoEmptyError | Conditions.NoOverlappingExceptions
-                   ->
-                   true
-                 | Conditions.DateComputation -> false)
-               scope_vcs.Conditions.vc_scope_list)
-        in
-        List.fold_left
-          (fun all_proven vc ->
-            if Z3backend.Io.check_vc decl_ctx scope_name scope_vcs vc then
-              all_proven
-            else false)
-          all_proven z3_vcs)
+        (* let z3_vcs = List.map (fun vc -> ( vc, try let ctx =
+           Z3backend.Io.make_context decl_ctx in let ctx =
+           Z3backend.Io.encode_asserts ctx scope_vcs.vc_scope_asserts in let
+           ctx, z3_vc = Z3backend.Io.translate_expr ctx vc.Conditions.vc_guard
+           in Z3backend.Io.Success (z3_vc, ctx) with Failure msg -> Fail msg ))
+           (List.filter (fun vc -> match vc.Conditions.vc_kind with |
+           Conditions.NoEmptyError | Conditions.NoOverlappingExceptions -> true
+           | Conditions.DateComputation -> false)
+           scope_vcs.Conditions.vc_scope_list) in let all_proven =
+           List.fold_left (fun all_proven vc -> if Z3backend.Io.check_vc
+           decl_ctx scope_name scope_vcs vc then all_proven else false)
+           all_proven z3_vcs in *)
+        all_proven)
       vcs true
   in
   if all_proven then

From 22faf1493275653ffdf7a7dca1fdba71837b6d24 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Tue, 27 Jun 2023 17:02:35 +0200
Subject: [PATCH 28/31] Big refactoring

---
 compiler/shared_ast/var.ml                 |   1 +
 compiler/shared_ast/var.mli                |   1 +
 compiler/verification/io.ml                |  31 +--
 compiler/verification/io.mli               |  22 +-
 compiler/verification/mopsabackend.real.ml | 239 +++++++++++----------
 compiler/verification/solver.ml            |  10 +-
 compiler/verification/z3backend.dummy.ml   |  10 +-
 compiler/verification/z3backend.mli        |   1 +
 compiler/verification/z3backend.real.ml    |   6 +-
 9 files changed, 158 insertions(+), 163 deletions(-)

diff --git a/compiler/shared_ast/var.ml b/compiler/shared_ast/var.ml
index 605185565..c21ed1437 100644
--- a/compiler/shared_ast/var.ml
+++ b/compiler/shared_ast/var.ml
@@ -107,6 +107,7 @@ module Map = struct
   let fold f m acc = fold (fun v x acc -> f (get v) x acc) m acc
   let filter f m = filter (fun k v -> f (get k) v) m
   let exists f m = exists (fun k v -> f (get k) v) m
+  let remove x s = remove (t x) s
 
   (* Add more as needed *)
 end
diff --git a/compiler/shared_ast/var.mli b/compiler/shared_ast/var.mli
index a3b69a2c8..047ad31c5 100644
--- a/compiler/shared_ast/var.mli
+++ b/compiler/shared_ast/var.mli
@@ -64,6 +64,7 @@ module Map : sig
   val empty : ('e, 'x) t
   val singleton : 'e var -> 'x -> ('e, 'x) t
   val add : 'e var -> 'x -> ('e, 'x) t -> ('e, 'x) t
+  val remove : 'e var -> ('e, 'x) t -> ('e, 'x) t
   val update : 'e var -> ('x option -> 'x option) -> ('e, 'x) t -> ('e, 'x) t
   val find : 'e var -> ('e, 'x) t -> 'x
   val find_opt : 'e var -> ('e, 'x) t -> 'x option
diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index 3cc800e48..4ea795217 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -37,27 +37,21 @@ module type Backend = sig
   val is_model_empty : model -> bool
 
   val translate_expr :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
+    Conditions.verification_conditions_scope ->
+    backend_context ->
+    typed Dcalc.Ast.expr ->
+    backend_context * vc_encoding
 
   val encode_asserts :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context
+    Conditions.verification_conditions_scope ->
+    backend_context ->
+    typed Dcalc.Ast.expr ->
+    backend_context
 end
 
 module type BackendIO = sig
-  val init_backend : unit -> unit
-
   type backend_context
-
-  val make_context : decl_ctx -> backend_context
-
   type vc_encoding
-
-  val translate_expr :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
-
-  val encode_asserts :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context
-
   type model
 
   type vc_encoding_result =
@@ -80,17 +74,8 @@ module type BackendIO = sig
 end
 
 module MakeBackendIO (B : Backend) = struct
-  let init_backend = B.init_backend
-
   type backend_context = B.backend_context
-
-  let make_context = B.make_context
-
   type vc_encoding = B.vc_encoding
-
-  let translate_expr = B.translate_expr
-  let encode_asserts = B.encode_asserts
-
   type model = B.model
 
   type vc_encoding_result =
diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli
index 6a232b0bb..4b47b550a 100644
--- a/compiler/verification/io.mli
+++ b/compiler/verification/io.mli
@@ -38,27 +38,21 @@ module type Backend = sig
   val is_model_empty : model -> bool
 
   val translate_expr :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
+    Conditions.verification_conditions_scope ->
+    backend_context ->
+    typed Dcalc.Ast.expr ->
+    backend_context * vc_encoding
 
   val encode_asserts :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context
+    Conditions.verification_conditions_scope ->
+    backend_context ->
+    typed Dcalc.Ast.expr ->
+    backend_context
 end
 
 module type BackendIO = sig
-  val init_backend : unit -> unit
-
   type backend_context
-
-  val make_context : decl_ctx -> backend_context
-
   type vc_encoding
-
-  val translate_expr :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
-
-  val encode_asserts :
-    backend_context -> typed Dcalc.Ast.expr -> backend_context
-
   type model
 
   type vc_encoding_result =
diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index 16b4ff640..b8b00e80d 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -18,13 +18,6 @@
 open Catala_utils
 open Shared_ast
 
-type mopsa_program = {
-  initial_guard : typed Dcalc.Ast.expr;
-  main_guard : typed Dcalc.Ast.expr;
-  declared_variables :
-    ((dcalc, typed) gexpr Var.t * typed Dcalc.Ast.expr option) list;
-}
-
 let simplified_string_of_pos pos =
   let basename =
     Filename.basename (Pos.get_file pos) |> Filename.chop_extension
@@ -33,56 +26,71 @@ let simplified_string_of_pos pos =
     (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
 
 let rec vars_used_in_vc vc_scope_ctx (e : typed Dcalc.Ast.expr) :
-    typed Dcalc.Ast.expr Var.Set.t =
+    (typed Dcalc.Ast.expr, typ) Var.Map.t =
+  let rec free_vars_with_types :
+      ('a, 't) gexpr -> (('a, 't) gexpr, typ) Var.Map.t =
+   fun e ->
+    match e with
+    | EVar v, _ -> Var.Map.singleton v (Expr.ty e)
+    | EAbs { binder; _ }, _ ->
+      let vs, body = Bindlib.unmbind binder in
+      Array.fold_right Var.Map.remove vs (free_vars_with_types body)
+    | e ->
+      Expr.shallow_fold
+        (fun e ->
+          Var.Map.union (fun _ _ -> assert false) (free_vars_with_types e))
+        e Var.Map.empty
+  in
+  let free_vars = free_vars_with_types e in
   (* We search recursively in the possible definitions of each free variable. *)
-  let free_vars = Expr.free_vars e in
   let possible_values_of_free_vars =
     Var.Map.filter
-      (fun v _ -> Var.Set.mem v free_vars)
+      (fun v _ -> Var.Map.mem v free_vars)
       vc_scope_ctx.Conditions.vc_scope_possible_variable_values
   in
   Var.Map.fold
     (fun _ possible_values vars_used ->
       List.fold_left
         (fun vars_used possible_value ->
-          Var.Set.union (vars_used_in_vc vc_scope_ctx possible_value) vars_used)
+          Var.Map.union
+            (fun _ _ -> assert false)
+            (vars_used_in_vc vc_scope_ctx possible_value)
+            vars_used)
         vars_used possible_values)
     possible_values_of_free_vars free_vars
 
+type mopsa_variable_declaration_value =
+  | Unknown of typ
+  | Known of typed Dcalc.Ast.expr
+
+type mopsa_program = {
+  initial_guard : typed Dcalc.Ast.expr;
+  main_guard : typed Dcalc.Ast.expr;
+  declared_variables :
+    ((dcalc, typed) gexpr Var.t * mopsa_variable_declaration_value) list;
+}
+
+type 'a mopsa_variable_declaration_boxed_value =
+  | BoxedUnknown of typ
+  | BoxedKnown of ('a, typed) marked
+
 module TypedValuesDcalcVarMap = struct
-  type 'x t = (typed Dcalc.Ast.expr, ('x, typed) marked option) Var.Map.t
+  type 'x t =
+    (typed Dcalc.Ast.expr, 'x mopsa_variable_declaration_boxed_value) Var.Map.t
 
   let map (f : 'a -> 'b) (m : 'a t) : 'b t =
-    Var.Map.map (Option.map (fun (x, tx) -> f x, tx)) m
+    Var.Map.map
+      (fun v ->
+        match v with
+        | BoxedUnknown ty -> BoxedUnknown ty
+        | BoxedKnown (e, te) -> BoxedKnown (f e, te))
+      m
 end
 
 module TypedValuesDcalcVarMapBoxLifting = Bindlib.Lift (TypedValuesDcalcVarMap)
 
-(** Sometimes VC contains struct accesses from larger values which are defined
-    elsewhere. Since MOPSA does not currently handle structs, etc., we prefer
-    replacing the struct access with its own variable coming with an unknown
-    value. *)
-let rec transform_field_accesses_into_variables
-    ~(is_vc_var : (dcalc, typed) naked_gexpr Bindlib.var -> bool)
-    (e : typed Dcalc.Ast.expr) :
-    (typed Dcalc.Ast.expr, typ) Var.Map.t * (dcalc, typed) boxed_gexpr =
-  match Mark.remove e with
-  | EStructAccess { e = EVar v, _; field; _ } when is_vc_var v ->
-    let var =
-      Var.make (Format.asprintf "%a__%a" Print.var v StructField.format_t field)
-    in
-    Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
-  | _ ->
-    Expr.map_gather ~acc:Var.Map.empty
-      ~join:(Var.Map.union (fun _ _ _ -> assert false))
-      ~f:(transform_field_accesses_into_variables ~is_vc_var)
-      e
-
 type mopsa_variable_declarations =
-  (typed Dcalc.Ast.expr, (dcalc, typed) gexpr option) Var.Map.t
-
-type mopsa_variable_boxed_declarations =
-  (typed Dcalc.Ast.expr, (dcalc, typed) boxed_gexpr option) Var.Map.t
+  (typed Dcalc.Ast.expr, mopsa_variable_declaration_value) Var.Map.t
 
 module VarVertex = struct
   include Var
@@ -103,11 +111,12 @@ let declaration_reverse_dependency_ordering (d : mopsa_variable_declarations) :
   let g = VarDependencies.empty in
   let g =
     Var.Map.fold
-      (fun (v : typed Dcalc.Ast.expr Var.t) (e : typed Dcalc.Ast.expr option) g ->
+      (fun (v : typed Dcalc.Ast.expr Var.t)
+           (e : mopsa_variable_declaration_value) g ->
         let g = VarDependencies.add_vertex g v in
         match e with
-        | None -> g
-        | Some e ->
+        | Unknown _ -> g
+        | Known e ->
           let used = Expr.free_vars e in
           Var.Set.fold (fun used g -> VarDependencies.add_edge g used v) used g)
       d g
@@ -117,7 +126,11 @@ let declaration_reverse_dependency_ordering (d : mopsa_variable_declarations) :
 (** To better split the load for MOPSA and improve debugging, we split the VC
     into smaller parts by creating supplementary variables. *)
 let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
-    mopsa_variable_boxed_declarations * (dcalc, typed) boxed_gexpr =
+    ( typed Dcalc.Ast.expr,
+      (dcalc, typed) naked_gexpr Bindlib.box
+      mopsa_variable_declaration_boxed_value )
+    Var.Map.t
+    * (dcalc, typed) boxed_gexpr =
   match Mark.remove e with
   | EApp
       {
@@ -144,29 +157,52 @@ let rec split_expression_into_atomic_parts (e : typed Dcalc.Ast.expr) :
       Var.make ("var_" ^ simplified_string_of_pos pos)
     in
     let new_e = Expr.eapp (Expr.box f) args (Mark.get e) in
-    Var.Map.add dummy_var (Some new_e) acc, Expr.evar dummy_var (Mark.get e)
+    ( Var.Map.add dummy_var (BoxedKnown new_e) acc,
+      Expr.evar dummy_var (Mark.get e) )
   | _ ->
     Expr.map_gather ~acc:Var.Map.empty
       ~join:(Var.Map.union (fun _ _ _ -> assert false))
       ~f:split_expression_into_atomic_parts e
 
+(** Sometimes VC contains struct accesses from larger values which are defined
+    elsewhere. Since MOPSA does not currently handle structs, etc., we prefer
+    replacing the struct access with its own variable coming with an unknown
+    value. *)
+let rec transform_field_accesses_into_variables
+    ~(is_vc_var : (dcalc, typed) naked_gexpr Bindlib.var -> bool)
+    (e : typed Dcalc.Ast.expr) :
+    (typed Dcalc.Ast.expr, typ) Var.Map.t * (dcalc, typed) boxed_gexpr =
+  match Mark.remove e with
+  | EStructAccess { e = EVar v, _; field; _ } when is_vc_var v ->
+    let var =
+      Var.make (Format.asprintf "%a__%a" Print.var v StructField.format_t field)
+    in
+    Var.Map.singleton var (Expr.ty e), Expr.evar var (Mark.get e)
+  | _ ->
+    Expr.map_gather ~acc:Var.Map.empty
+      ~join:(Var.Map.union (fun _ _ _ -> assert false))
+      ~f:(transform_field_accesses_into_variables ~is_vc_var)
+      e
+
 (* The goal of this part is to extract additions from expressions, and perform
    them before as assignments. This will simplify the analysis and communication
    with Mopsa. *)
 let translate_expr
     (vc_scope_ctx : Conditions.verification_conditions_scope)
-    (original_vc_guard : typed Dcalc.Ast.expr) =
+    (original_vc_guard : typed Dcalc.Ast.expr) : mopsa_program =
   let vars_used_in_vc = vars_used_in_vc vc_scope_ctx original_vc_guard in
   let vars_used_in_vc_with_known_values =
-    Var.Set.filter
-      (fun v ->
+    Var.Map.filter
+      (fun v _ ->
         Var.Map.mem v vc_scope_ctx.Conditions.vc_scope_possible_variable_values)
       vars_used_in_vc
   in
   let vc_variables_declarations_unknown =
-    Var.Set.fold
-      (fun v declarations -> Var.Map.add v None declarations)
-      (Var.Set.diff vars_used_in_vc vars_used_in_vc_with_known_values)
+    Var.Map.fold
+      (fun v ty declarations -> Var.Map.add v (Unknown ty) declarations)
+      (Var.Map.filter
+         (fun v _ -> not (Var.Map.mem v vars_used_in_vc_with_known_values))
+         vars_used_in_vc)
       Var.Map.empty
   in
   let vc_variables_declarations_defined =
@@ -177,17 +213,17 @@ let translate_expr
             "Only the first possible value was taken into account for %a"
             Print.var_debug var;
         (* FIXME: take into account multiple possible values *)
-        Some (List.hd values))
+        Known (List.hd values))
       (Var.Map.filter
-         (fun v _ -> Var.Set.mem v vars_used_in_vc)
+         (fun v _ -> Var.Map.mem v vars_used_in_vc)
          vc_scope_ctx.vc_scope_possible_variable_values)
   in
-  let vc_variables_declarations =
+  let vc_variables_declarations : mopsa_variable_declarations =
     Var.Map.union
       (fun _ _ -> assert false)
       vc_variables_declarations_unknown vc_variables_declarations_defined
   in
-  let new_vars_for_struct_accesses, (vc_guard, vc_guard_mark) =
+  let new_vars_for_struct_accesses, vc_guard =
     transform_field_accesses_into_variables
       ~is_vc_var:(fun v ->
         Var.Map.exists
@@ -195,24 +231,10 @@ let translate_expr
           vc_variables_declarations)
       original_vc_guard
   in
-  let new_vars_for_struct_accesses, vc_scope_ctx =
-    ( Var.Map.map (fun _ -> None) new_vars_for_struct_accesses,
-      {
-        vc_scope_ctx with
-        vc_scope_variables_typs =
-          Var.Map.union
-            (fun _ _ _ -> assert false)
-            vc_scope_ctx.vc_scope_variables_typs new_vars_for_struct_accesses;
-      } )
-  in
-  let new_vars_for_struct_accesses, vc_guard =
-    Bindlib.unbox
-      (Bindlib.box_apply2
-         (fun new_vars_for_struct_accesses vc_guard ->
-           new_vars_for_struct_accesses, (vc_guard, vc_guard_mark))
-         (TypedValuesDcalcVarMapBoxLifting.lift_box new_vars_for_struct_accesses)
-         vc_guard)
+  let new_vars_for_struct_accesses : mopsa_variable_declarations =
+    Var.Map.map (fun ty -> Unknown ty) new_vars_for_struct_accesses
   in
+  let vc_guard = Expr.unbox vc_guard in
   let new_vars_for_atomic_splitting, (vc_guard, vc_guard_mark) =
     split_expression_into_atomic_parts vc_guard
   in
@@ -227,6 +249,12 @@ let translate_expr
             new_vars_for_atomic_splitting)
          vc_guard)
   in
+  let new_vars_for_atomic_splitting : mopsa_variable_declarations =
+    Var.Map.map
+      (fun v ->
+        match v with BoxedUnknown ty -> Unknown ty | BoxedKnown e -> Known e)
+      new_vars_for_atomic_splitting
+  in
   let vc_variables_declarations =
     Var.Map.union
       (fun _ _ -> assert false)
@@ -238,21 +266,18 @@ let translate_expr
   let declaration_reverse_dependency_ordering =
     declaration_reverse_dependency_ordering vc_variables_declarations
   in
-  ( vc_scope_ctx,
-    {
-      initial_guard = original_vc_guard;
-      main_guard = vc_guard;
-      declared_variables =
-        (* Careful with the order! these definitions must be laid out in reverse
-           dependency order *)
-        List.map
-          (fun v -> v, Var.Map.find v vc_variables_declarations)
-          declaration_reverse_dependency_ordering;
-    } )
-
-let print_encoding
-    (vc_scope_ctx : Conditions.verification_conditions_scope)
-    (prog : mopsa_program) =
+  {
+    initial_guard = original_vc_guard;
+    main_guard = vc_guard;
+    declared_variables =
+      (* Careful with the order! these definitions must be laid out in reverse
+         dependency order *)
+      List.map
+        (fun v -> v, Var.Map.find v vc_variables_declarations)
+        declaration_reverse_dependency_ordering;
+  }
+
+let print_encoding (prog : mopsa_program) =
   let fmt = Format.str_formatter in
   let () =
     Format.fprintf fmt "%aassert(sync(%a));@."
@@ -260,31 +285,7 @@ let print_encoding
          ~pp_sep:(fun _ () -> ())
          (fun fmt (var, oexpr) ->
            match oexpr with
-           | None -> (
-             let ty =
-               match
-                 Var.Map.find_opt var vc_scope_ctx.vc_scope_variables_typs
-               with
-               | None ->
-                 (* FIXME: I may have added to many variables in
-                    vc_scope_variables_typs in commit b08841e7, the good way to
-                    do it would be to extract types of variables from the
-                    expression directly *)
-                 let rec find_type_of_var v e =
-                   match e with
-                   | EVar v', mark when Var.compare v v' = 0 -> [mark]
-                   | e ->
-                     Expr.shallow_fold
-                       (fun e acc -> find_type_of_var v e @ acc)
-                       e []
-                 in
-                 let m = find_type_of_var var prog.initial_guard in
-                 (* let () = Message.emit_debug "searching for %a in %a"
-                    Print.var_debug var (Print.expr ()) prog.initial_guard in *)
-                 let (Typed { ty; _ }) = List.hd m in
-                 ty
-               | Some ty -> ty
-             in
+           | Unknown ty -> (
              let make_random =
                match Mark.remove ty with
                | TLit TDate -> Some "date()"
@@ -300,7 +301,7 @@ let print_encoding
              | None ->
                Message.emit_debug "Ignoring type declaration of var %a : %a"
                  Print.var_debug var Print.typ_debug ty)
-           | Some expr ->
+           | Known expr ->
              Format.fprintf fmt "%a %a = %a;@." Print.typ_debug (Expr.ty expr)
                Print.var var
                (Print.expr ~debug:false ())
@@ -312,16 +313,22 @@ let print_encoding
   let str = Format.flush_str_formatter () in
   String.to_ascii str
 
-module Backend = struct
+module Backend : Io.Backend = struct
   type vc_encoding = mopsa_program
 
   let init_backend () = ()
 
-  type backend_context = Conditions.verification_conditions_scope
+  type backend_context = unit
+
+  let make_context _ = ()
+
+  let translate_expr
+      (scope_vcs : Conditions.verification_conditions_scope)
+      ()
+      (e : typed Dcalc.Ast.expr) : unit * mopsa_program =
+    (), translate_expr scope_vcs e
 
-  let make_context _ = assert false
-  let translate_expr = translate_expr
-  let print_encoding ctx prog = print_encoding ctx prog
+  let print_encoding _ctx prog = print_encoding prog
 
   type model = Yojson.Basic.t (* yeah, I'll have to fix that *)
   type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
@@ -392,7 +399,7 @@ module Backend = struct
   let print_model _ m : string = Yojson.Basic.pretty_to_string ~std:true m
   let init_backend () = Message.emit_debug "Running Mopsa"
   let is_model_empty _ = false
-  let encode_asserts _ _ = assert false
+  let encode_asserts _ _ _ = assert false
 end
 
 module Io = Io.MakeBackendIO (Backend)
diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index bd4985993..b69203576 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -25,11 +25,12 @@ let solve_vcs
     (vcs : Conditions.verification_conditions_scope ScopeName.Map.t) : unit =
   (* Right now we only use the Z3 backend but the functorial interface should
      make it easy to mix and match different proof backends. *)
-  Z3backend.Io.init_backend ();
-  Mopsabackend.Io.init_backend ();
+  Z3backend.Backend.init_backend ();
+  Mopsabackend.Backend.init_backend ();
   let all_proven =
     ScopeName.Map.fold
-      (fun scope_name scope_vcs all_proven ->
+      (fun scope_name (scope_vcs : Conditions.verification_conditions_scope)
+           all_proven ->
         let dates_vcs =
           List.filter
             (fun vc ->
@@ -39,7 +40,8 @@ let solve_vcs
             scope_vcs.Conditions.vc_scope_list
           |> List.map (fun vc ->
                  let ctx, prog =
-                   Mopsabackend.Io.translate_expr scope_vcs
+                   Mopsabackend.Backend.translate_expr scope_vcs
+                     (Mopsabackend.Backend.make_context decl_ctx)
                      vc.Conditions.vc_guard
                  in
                  vc, Mopsabackend.Io.Success (prog, ctx))
diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml
index 37bddf1a9..5680f1a15 100644
--- a/compiler/verification/z3backend.dummy.ml
+++ b/compiler/verification/z3backend.dummy.ml
@@ -21,7 +21,7 @@ let dummy () =
   Catala_utils.Message.raise_error
     "This instance of Catala was compiled without Z3 support."
 
-module Io = struct
+module Backend = struct
   let init_backend () = dummy ()
 
   type backend_context = unit
@@ -30,9 +30,13 @@ module Io = struct
 
   type vc_encoding = unit
 
-  let translate_expr _ _ = dummy ()
-  let encode_asserts _ _ = dummy ()
+  let translate_expr _ _ _ = dummy ()
+  let encode_asserts _ _ _ = dummy ()
+end
 
+module Io = struct
+  type backend_context = unit
+  type vc_encoding = unit
   type model = unit
   type vc_encoding_result = Success of model * model | Fail of string
 
diff --git a/compiler/verification/z3backend.mli b/compiler/verification/z3backend.mli
index e43807b02..7b35b75bb 100644
--- a/compiler/verification/z3backend.mli
+++ b/compiler/verification/z3backend.mli
@@ -17,4 +17,5 @@
 
 (** Interfacing with the Z3 SMT solver *)
 
+module Backend : Io.Backend
 module Io : Io.BackendIO
diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml
index ff6c546ff..871f627e2 100644
--- a/compiler/verification/z3backend.real.ml
+++ b/compiler/verification/z3backend.real.ml
@@ -817,11 +817,11 @@ module Backend = struct
 
   let is_model_empty (m : model) : bool = Z3.Model.get_decls m = []
 
-  let translate_expr (ctx : backend_context) (e : typed expr) =
+  let translate_expr _ (ctx : backend_context) (e : typed expr) =
     translate_expr ctx e
 
-  let encode_asserts (ctx : backend_context) (e : typed expr) =
-    let ctx, vc = translate_expr ctx e in
+  let encode_asserts scvs (ctx : backend_context) (e : typed expr) =
+    let ctx, vc = translate_expr scvs ctx e in
     add_z3constraint vc ctx
 
   let init_backend () =

From 97b87099d87a3c1d8fbc5f0e5e6d0be47cd9cc96 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Thu, 7 Dec 2023 15:31:46 +0100
Subject: [PATCH 29/31] More informative warning and debug messages when Mopsa
 cannot analyze the program

---
 compiler/verification/mopsabackend.real.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/compiler/verification/mopsabackend.real.ml b/compiler/verification/mopsabackend.real.ml
index b8b00e80d..b448be6db 100644
--- a/compiler/verification/mopsabackend.real.ml
+++ b/compiler/verification/mopsabackend.real.ml
@@ -357,7 +357,10 @@ module Backend : Io.Backend = struct
         Some (Yojson.Basic.from_string new_json_to_parse)
       else
         let () =
-          Message.emit_warning "Something went wrong with Mopsa: %s"
+          Message.emit_warning "Mopsa failed to analyze %s"
+            prog_name in
+        let () =
+          Message.emit_debug "Mopsa failed with message:\n%s"
             (j |> member "exception" |> to_string)
         in
         None

From 4413af3e5eba7f8e107b60c5f24f3b6a1afccaf5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Fri, 8 Dec 2023 11:02:45 +0100
Subject: [PATCH 30/31] Tweak ppx_yojson version

---
 catala.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/catala.opam b/catala.opam
index a98e01242..4917d14e6 100644
--- a/catala.opam
+++ b/catala.opam
@@ -31,7 +31,7 @@ depends: [
   "ocaml" {>= "4.13.0"}
   "ocamlfind" {!= "1.9.5"}
   "ocamlgraph" {>= "1.8.8"}
-  "ppx_yojson_conv" {>= "0.14.0"}
+  "ppx_yojson_conv" {= "v0.15.1"}
   "re" {>= "1.9.0"}
   "sedlex" {>= "2.4"}
   "uutf" {>= "1.0.3"}

From ad81409e37ea9de3187e7e8dbb68ce41bd0a2702 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= <raphael.monat@inria.fr>
Date: Fri, 8 Dec 2023 16:07:13 +0100
Subject: [PATCH 31/31] Fix dummy z3 backend with compatible IO interface

---
 compiler/verification/solver.ml          | 2 +-
 compiler/verification/z3backend.dummy.ml | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml
index b69203576..b84ecd9c3 100644
--- a/compiler/verification/solver.ml
+++ b/compiler/verification/solver.ml
@@ -25,7 +25,7 @@ let solve_vcs
     (vcs : Conditions.verification_conditions_scope ScopeName.Map.t) : unit =
   (* Right now we only use the Z3 backend but the functorial interface should
      make it easy to mix and match different proof backends. *)
-  Z3backend.Backend.init_backend ();
+  (* Z3backend.Backend.init_backend (); *)
   Mopsabackend.Backend.init_backend ();
   let all_proven =
     ScopeName.Map.fold
diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml
index 5680f1a15..af084ffd2 100644
--- a/compiler/verification/z3backend.dummy.ml
+++ b/compiler/verification/z3backend.dummy.ml
@@ -30,6 +30,15 @@ module Backend = struct
 
   type vc_encoding = unit
 
+  let print_encoding _ _ = dummy ()
+
+  type model = unit
+  type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
+
+  let solve_vc_encoding _ _ = dummy ()
+  let print_model _ _ = dummy ()
+  let is_model_empty _ = dummy () 
+
   let translate_expr _ _ _ = dummy ()
   let encode_asserts _ _ _ = dummy ()
 end