Proven one more subcase

doc/formalization/Catala.LambdaCalculus.fst

@@ -53,7 +53,6 @@ val is_value: exp -> Tot bool
 let rec is_value e =
   match e with
   | EAbs _ _ | EThunk _ | ELit _ | ENone -> true
-  | ESome (ELit (LError _)) -> false
   | ESome e' -> is_value e'
   | EList l -> is_value_list l
   | _ -> false
@@ -750,6 +749,7 @@ and preservation_list
 
 let identity_var_to_exp : var_to_exp = fun x -> EVar x
 
+#push-options "--fuel 3 --ifuel 2"
 let rec subst_by_identity_is_identity (e: exp) : Lemma (subst identity_var_to_exp e == e) =
   match e with
   | EVar _ -> ()
@@ -788,7 +788,7 @@ and subst_by_identity_is_identity_list (l: list exp) : Lemma (subst_list identit
   | hd::tl ->
     subst_by_identity_is_identity hd;
     subst_by_identity_is_identity_list tl
-
+#pop-options
 
 let typing_empty_can_be_extended (e: exp) (tau: ty) (g: env)
     : Lemma

doc/formalization/Catala.Translation.Helpers.fst

@@ -1,6 +1,7 @@
 module Catala.Translation.Helpers
 
 open Catala.LambdaCalculus
+module T = FStar.Tactics
 
 (*** Default translation *)
 
@@ -623,3 +624,54 @@ let step_exceptions_head_value_same_acc_result
     )
   =
   admit()
+
+let step_exceptions_empty_conflict_error
+  (tau: ty)
+  (just: (typed_l_exp TBool))
+  (cons: (typed_l_exp tau))
+    : Pure nat
+      (requires (True))
+      (ensures (fun n ->
+      build_default_translation_typing [] (ELit (LError ConflictError)) just cons tau empty;
+        take_l_steps tau
+          (build_default_translation [] (ELit (LError ConflictError)) just cons tau) n ==
+            Some (ELit (LError ConflictError))))
+  =
+  build_default_translation_typing [] (ELit (LError ConflictError)) just cons tau empty;
+  assert_norm(take_l_steps tau
+          (build_default_translation [] (ELit (LError ConflictError)) just cons tau) 2 ==
+            Some (ELit (LError ConflictError)));
+  2
+
+#push-options "--fuel 4 --ifuel 1 --z3rlimit 40"
+let step_exceptions_empty_some_acc
+  (tau: ty)
+  (just: (typed_l_exp TBool))
+  (cons: (typed_l_exp tau))
+  (acc: (typed_l_exp tau))
+    : Pure nat
+      (requires (is_value acc))
+      (ensures (fun n ->
+      build_default_translation_typing [] (ESome acc) just cons tau empty;
+        take_l_steps tau
+          (build_default_translation [] (ESome acc) just cons tau) n ==
+            Some acc))
+  =
+  let one_step : typed_l_exp tau =
+    EMatchOption (ESome acc) tau
+              (EIf just cons (ELit (LError (EmptyError))))
+              (EAbs tau (EVar 0))
+  in
+  build_default_translation_typing [] (ESome acc) just cons tau empty;
+  assert(take_l_steps tau
+          (build_default_translation [] (ESome acc) just cons tau) 1 ==
+            Some one_step);
+  let two_step : typed_l_exp tau =
+    EApp (EAbs tau (EVar 0)) acc tau
+  in
+  assert(take_l_steps tau one_step 1 == Some two_step);
+  assert(take_l_steps tau two_step 1 == Some acc);
+  take_l_steps_transitive tau (build_default_translation [] (ESome acc) just cons tau) one_step 1 1;
+  take_l_steps_transitive tau (build_default_translation [] (ESome acc) just cons tau) two_step 2 1;
+  3
+#pop-options

doc/formalization/Catala.Translation.fst

@@ -637,7 +637,7 @@ let dacc_lacc_sync
   =
   match dacc, lacc with
   | D.AllEmpty, L.ENone -> True
-  | D.OneNonEmpty de', L.ESome le' -> le' == translate_exp de'
+  | D.OneNonEmpty de', L.ESome le' -> le' == translate_exp de' /\ L.is_value le'
   | D.Conflict, L.ELit (L.LError L.ConflictError) -> True
   | _ -> False
 
@@ -689,8 +689,24 @@ let rec translation_correctness_exceptions_empty_count_exception_triggered
       ))
       (decreases dexceptions)
   =
+  translation_preserves_typ_exceptions D.empty de dexceptions dtau;
+  translation_preserves_empty_typ djust D.TBool;
+  translation_preserves_empty_typ dcons dtau;
+  let ljust = translate_exp djust in
+  let lcons = translate_exp dcons in
+  let ltau = translate_ty dtau in
+  let l_err : typed_l_exp ltau = L.ELit (L.LError L.ConflictError) in
   match dexceptions with
-  | [] -> admit()
+  | [] -> begin
+    match lacc with
+    | L.ELit (L.LError L.ConflictError) ->
+      let n_err = step_exceptions_empty_conflict_error ltau ljust lcons in
+      n_err, l_err
+    | L.ESome lacc_inner ->
+      assert(L.is_value lacc_inner);
+      let n = step_exceptions_empty_some_acc ltau ljust lcons lacc_inner in
+      n, lacc_inner
+  end
   | dhd::dtl -> admit()
 #pop-options