Some proof progress

doc/formalization/Catala.Translation.Helpers.fst

@@ -286,7 +286,7 @@ let exceptions_head_lift'
     typ_process_exceptions_f empty tau;
     typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau));
     typing_empty_can_be_extended acc (TOption tau)
-    (extend (extend empty (TOption tau)) tau);
+      (extend (extend empty (TOption tau)) tau);
     EMatchOption
     (EFoldLeft
       (process_exceptions_f tau)
@@ -576,7 +576,27 @@ let exceptions_head_lift_steps_to_error
   take_l_steps_transitive tau e e_plus_4 4 1
 #pop-options
 
+#push-options "--fuel 4 --ifuel 1 --z3rlimit 20"
+let exception_init_lift_conflict_error
+  (tau: ty)
+  (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
+  (just: (typed_l_exp TBool))
+  (cons: (typed_l_exp tau))
+    : Lemma (
+      take_l_steps tau (exceptions_init_lift tau tl just cons (ELit (LError ConflictError))) 2 ==
+        Some (ELit (LError ConflictError)))
+  =
+  let c_err = ELit (LError ConflictError) in
+  let e0 = exceptions_init_lift tau tl just cons (ELit (LError ConflictError)) in
+  let e1 = EMatchOption c_err tau (EIf just cons (ELit (LError EmptyError))) (EAbs tau (EVar 0)) in
+  assert(step e0 == Some e1);
+  assert(step e1 == Some c_err);
+  preservation e0 tau;
+  preservation e1 tau;
+  take_l_steps_transitive tau e0 e1 1 1
+#pop-options
 
+#push-options "--fuel 8 --ifuel 1 --z3rlimit 150"
 let step_exceptions_head_value
   (tau: ty)
   (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
@@ -585,20 +605,82 @@ let step_exceptions_head_value
   (cons: (typed_l_exp tau))
   (hd: (typed_l_exp tau))
     : Pure (typed_l_exp (TOption tau) & nat)
-      (requires (is_value hd))
+      (requires (is_value hd /\ is_value acc))
       (ensures (fun (new_acc, n) ->
         is_value new_acc /\
         take_l_steps tau (exceptions_head_lift tau tl acc just cons hd) n ==
           Some (exceptions_init_lift tau tl just cons new_acc)
       ))
   =
-  admit()
+  typ_process_exceptions_f empty tau;
+  typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau));
+  typing_empty_can_be_extended acc (TOption tau)
+    (extend (extend empty (TOption tau)) tau);
+  let init0 : typed_l_exp (TOption tau) = EApp (EAbs (TOption tau) (
+    EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
+      ELit (LError ConflictError))))))) (ECatchEmptyError (ESome hd) ENone) (TOption tau)
+  in
+  let match_arg0  =
+    EFoldLeft (process_exceptions_f tau) init0 (TOption tau) (EList tl) (TArrow TUnit tau)
+  in
+  let c_err = ELit (LError ConflictError) in
+  let match_none0 = EIf just cons (ELit (LError EmptyError)) in
+  let match_some0 = EAbs tau (EVar 0) in
+  assert(exceptions_head_lift tau tl acc just cons hd ==
+    EMatchOption match_arg0 tau match_none0 match_some0);
+  assert(exceptions_head_lift tau tl acc just cons hd ==
+    exceptions_init_lift tau tl just cons init0);
+  let acc_invariant (s: var_to_exp) : Lemma (subst s acc == acc) [SMTPat (subst s acc)] =
+    well_typed_terms_invariant_by_subst s acc (TOption tau)
+  in
+  match hd with
+  | ELit (LError err) ->
+    let init1 = EApp (EAbs (TOption tau) (
+      EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
+        ELit (LError ConflictError))))))) (ECatchEmptyError hd ENone) (TOption tau)
+    in
+    assert(step init0 == Some init1);
+    begin match err with
+    | ConflictError ->
+      let init2 = EApp (EAbs (TOption tau) (
+        EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
+          ELit (LError ConflictError))))))) hd (TOption tau)
+      in
+      assert(step init1 == Some init2);
+      assert(step init2 == Some c_err);
+      preservation init0 (TOption tau);
+      preservation init1 (TOption tau);
+      preservation init2 (TOption tau);
+      take_l_steps_transitive (TOption tau) init0 init1 1 1;
+      take_l_steps_transitive (TOption tau) init0 init2 2 1;
+      assert(take_l_steps (TOption tau) init0 3 == Some c_err);
+      lift_multiple_l_steps (TOption tau) tau init0 c_err 3
+        (exceptions_init_lift tau tl just cons);
+      assert(take_l_steps tau (exceptions_head_lift tau tl acc just cons hd) 3 ==
+        Some (exceptions_init_lift tau tl just cons c_err));
+      exception_init_lift_conflict_error tau tl just cons;
+      c_err, 3
+    | EmptyError ->
+      let init2 = EApp (EAbs (TOption tau) (
+        EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
+          ELit (LError ConflictError))))))) ENone (TOption tau)
+      in
+      assert(step init1 == Some init2);
+      let init3 =
+        EMatchOption acc tau ENone (EAbs tau (EMatchOption ENone tau acc (EAbs tau (
+          ELit (LError ConflictError)))))
+      in
+      assert(step init2 == Some init3);
+      admit()
+    end
+  | _ -> admit()
+#pop-options
 
 let step_exceptions_head_value_same_acc_result
   (tau: ty)
   (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
   (tl': list exp{is_value_list tl' /\ typing_list empty tl' (TArrow TUnit tau)})
-  (acc: (typed_l_exp (TOption tau)))
+  (acc: typed_l_exp (TOption tau){is_value acc})
   (just: (typed_l_exp TBool))
   (cons: (typed_l_exp tau))
   (hd: (typed_l_exp tau){is_value hd})

doc/formalization/Catala.Translation.fst

@@ -656,6 +656,7 @@ let step_exceptions_head_value_source_acc_synced_dacc
       (requires (
         dacc_lacc_sync (translate_ty dtau) dacc lacc /\
         D.typing D.empty dhd dtau /\ D.is_value dhd /\
+        L.is_value lacc /\
         dacc <> D.Conflict
       ))
       (ensures (fun new_dacc ->