diff --git a/doc/formalization/Catala.DefaultCalculus.fst b/doc/formalization/Catala.DefaultCalculus.fst index 3eadd404..c6e8cbd1 100644 --- a/doc/formalization/Catala.DefaultCalculus.fst +++ b/doc/formalization/Catala.DefaultCalculus.fst @@ -89,6 +89,11 @@ type empty_count_result = | OneNonEmpty of exp | Conflict +type exceptions_count_result = + | NoStep + | IllFormed + | SomeStep of exp + let rec empty_count (acc: empty_count_result) (l: list exp) : Tot empty_count_result (decreases l) = match l with | [] -> acc @@ -178,14 +183,17 @@ and step_exceptions (just: exp{just << e}) (cons: exp{cons << e}) (tau: ty) - : Tot (option exp) (decreases %[ e; 3 ]) = - if List.Tot.for_all (fun except -> is_value except) exceptions + : Tot exceptions_count_result (decreases %[ e; 3 ]) = + if List.Tot.for_all is_value exceptions then match empty_count AllEmpty exceptions with - | AllEmpty -> None - | OneNonEmpty e' -> Some e' (* D-DefaultOneException *) - | Conflict -> Some (ELit LConflictError) (* D-DefaultExceptionConflict *) - else step_exceptions_left_to_right e exceptions just cons tau + | AllEmpty -> NoStep + | OneNonEmpty e' -> SomeStep e' (* D-DefaultOneException *) + | Conflict -> SomeStep (ELit LConflictError) (* D-DefaultExceptionConflict *) + else + match step_exceptions_left_to_right e exceptions just cons tau with + | None -> IllFormed + | Some e' -> SomeStep e' and step_default (e: exp) @@ -195,22 +203,16 @@ and step_default (tau: ty) : Tot (option exp) (decreases %[ e; 4 ]) = match step_exceptions e exceptions just cons tau with - | Some e' -> Some e' - | None -> + | IllFormed -> None + | SomeStep e' -> Some e' + | NoStep -> if is_value just then match just with | ELit LConflictError -> Some c_err (* D-ContextConflictError *) | ELit LEmptyError -> Some e_err (* D-ContextEmptyError *) | _ -> match just with - | ELit LTrue -> - if is_value cons - then Some cons - else - (match (step cons) with - | Some (ELit LConflictError) -> Some c_err (* D-ContextConflictError *) - | Some cons' -> Some (EDefault exceptions just cons' tau) (* D-DefaultTrueNoExceptions*) - | None -> None) + | ELit LTrue -> Some cons (* D-DefaultTrueNoExceptions*) | ELit LFalse -> Some e_err (* D-DefaultFalseNoExceptions *) | _ -> None else @@ -282,7 +284,7 @@ let typing_conserved_by_list_reduction (g: env) (subs: list exp) (tau: ty) (**** Progress theorem *) -#push-options "--fuel 2 --ifuel 1" +#push-options "--fuel 2 --ifuel 1 --z3rlimit 20" let rec progress (e: exp) (tau: ty) : Lemma (requires (typing empty e tau)) (ensures (is_value e \/ (Some? (step e)))) @@ -305,14 +307,17 @@ and progress_default (cons: exp{cons << e}) (tau: ty) : Lemma (requires ( - ~(is_value e) /\ e == EDefault exceptions just cons tau /\ (typing empty e tau) )) (ensures (Some? (step_default e exceptions just cons tau))) (decreases %[ e; 2 ]) = match step_exceptions e exceptions just cons tau with - | Some _ -> () - | None -> + | IllFormed -> + assert(step_exceptions_left_to_right e exceptions just cons tau == None); + assert(~(List.Tot.for_all is_value exceptions)); + progress_default_exceptions e exceptions just cons tau + | SomeStep _ -> () + | NoStep -> if is_value just then (is_bool_value_cannot_be_abs empty just; match just, cons with @@ -322,6 +327,27 @@ and progress_default | ELit LEmptyError, _ -> () | ELit LConflictError, _ -> ()) else progress just TBool +and progress_default_exceptions + (e: exp) + (exceptions: list exp {exceptions << e}) + (just: exp{just << e}) + (cons: exp{cons << e}) + (tau: ty) + : Lemma (requires ( + typing_list empty exceptions tau /\ + step_exceptions_left_to_right e exceptions just cons tau == None /\ + ~(List.Tot.for_all is_value exceptions) + )) + (ensures (False)) + (decreases %[ e; 1; exceptions ]) + = + match exceptions with + | [] -> () + | hd::tl -> + progress hd tau; + if is_value hd then begin + progress_default_exceptions e tl just cons tau + end else () #pop-options (*** Preservation *) @@ -504,7 +530,7 @@ let rec preservation (e: exp) (tau: ty) match empty_count AllEmpty exceptions with | AllEmpty -> begin if not (is_value just) then preservation just TBool else match just with - | ELit LTrue -> if not (is_value cons) then preservation cons tau + | ELit LTrue -> () | _ -> () end | OneNonEmpty e' -> empty_count_preserves_type AllEmpty exceptions empty tau diff --git a/doc/formalization/Catala.Translation.fst b/doc/formalization/Catala.Translation.fst index 3ef09729..92a0f9a2 100644 --- a/doc/formalization/Catala.Translation.fst +++ b/doc/formalization/Catala.Translation.fst @@ -810,14 +810,16 @@ let translation_correctness_exceptions_step Some? (D.step de) /\ de == D.EDefault dexceptions djust dcons dtau /\ D.typing D.empty de dtau /\ - D.step de == D.step_exceptions de dexceptions djust dcons dtau + (match D.step de, D.step_exceptions de dexceptions djust dcons dtau with + | Some de', D.SomeStep de'' -> de' == de'' + | _ -> False) )) (ensures (fun (n1, target_e, n2) -> translation_preserves_empty_typ de dtau; let lexceptions = translate_exp_list dexceptions in let ljust = translate_exp djust in let lcons = translate_exp dcons in - let Some de' = D.step_exceptions de dexceptions djust dcons dtau in + let D.SomeStep de' = D.step_exceptions de dexceptions djust dcons dtau in let le' = translate_exp de' in D.preservation de dtau; let ltau = translate_ty dtau in @@ -835,7 +837,49 @@ let translation_correctness_exceptions_step end else translation_correctness_exceptions_left_to_right_step de dexceptions djust dcons dtau L.ENone rec_lemma +#pop-options +let final_default_subexp + (tau: L.ty) + (just: typed_l_exp L.TBool) (cons: typed_l_exp tau) + : Tot (typed_l_exp tau) + = + L.EIf just cons (L.ELit (L.LError L.EmptyError)) + +#push-options "--fuel 2 --ifuel 1 --z3rlimit 150" +let translation_correctness_exceptions_no_exceptions_triggered + (de: D.exp) + (dexceptions: list D.exp {dexceptions << de}) + (djust: D.exp{djust << de}) + (dcons: D.exp{dcons << de}) + (dtau: D.ty) + : Pure nat + (requires ( + D.typing D.empty de dtau /\ + D.typing_list D.empty dexceptions dtau /\ + D.typing D.empty djust D.TBool /\ + D.typing D.empty dcons dtau /\ + List.Tot.for_all D.is_value dexceptions /\ + (D.step de == D.step_default de dexceptions djust dcons dtau) /\ + (D.step_exceptions de dexceptions djust dcons dtau == D.NoStep) + )) + (ensures (fun n -> + translate_empty_is_empty (); + translation_preserves_typ_exceptions D.empty de dexceptions dtau; + translation_preserves_empty_typ djust D.TBool; + translation_preserves_empty_typ dcons dtau; + let lexceptions = translate_exp_list dexceptions in + 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 + build_default_translation_typing lexceptions L.ENone ljust lcons ltau L.empty; + take_l_steps ltau (build_default_translation lexceptions L.ENone ljust lcons ltau) n + == Some (final_default_subexp ltau ljust lcons) + )) + (decreases dexceptions) + = + admit() #pop-options #push-options "--fuel 2 --ifuel 1 --z3rlimit 50" @@ -864,41 +908,41 @@ let rec translation_correctness_step (de: D.exp) (dtau: D.ty) | D.ELit _ -> 0, le, 0 | D.EAbs _ _ -> 0, le, 0 | D.EIf de1 de2 de3 -> - let le1 = translate_exp de1 in - let le2 = translate_exp de2 in - let le3 = translate_exp de3 in - if not (D.is_value de1) then begin - let de1' = Some?.v (D.step de1) in - D.preservation de1 D.TBool; - translation_preserves_empty_typ de1 D.TBool; - translation_preserves_empty_typ de2 dtau; - translation_preserves_empty_typ de3 dtau; - translation_preserves_empty_typ de1' D.TBool; - let le1' : typed_l_exp L.TBool = translate_exp de1' in - let n1_e1, target_e1, n2_e1 = translation_correctness_step de1 D.TBool in - assert(take_l_steps L.TBool le1 n1_e1 == Some target_e1); - assert(take_l_steps L.TBool le1' n2_e1 == Some target_e1); - lift_multiple_l_steps L.TBool ltau le1 target_e1 n1_e1 - (if_cond_lift ltau le2 le3); - lift_multiple_l_steps L.TBool ltau le1' target_e1 n2_e1 - (if_cond_lift ltau le2 le3); - n1_e1, if_cond_lift ltau le2 le3 target_e1, n2_e1 - end else (1, le', 0) + let le1 = translate_exp de1 in + let le2 = translate_exp de2 in + let le3 = translate_exp de3 in + if not (D.is_value de1) then begin + let de1' = Some?.v (D.step de1) in + D.preservation de1 D.TBool; + translation_preserves_empty_typ de1 D.TBool; + translation_preserves_empty_typ de2 dtau; + translation_preserves_empty_typ de3 dtau; + translation_preserves_empty_typ de1' D.TBool; + let le1' : typed_l_exp L.TBool = translate_exp de1' in + let n1_e1, target_e1, n2_e1 = translation_correctness_step de1 D.TBool in + assert(take_l_steps L.TBool le1 n1_e1 == Some target_e1); + assert(take_l_steps L.TBool le1' n2_e1 == Some target_e1); + lift_multiple_l_steps L.TBool ltau le1 target_e1 n1_e1 + (if_cond_lift ltau le2 le3); + lift_multiple_l_steps L.TBool ltau le1' target_e1 n2_e1 + (if_cond_lift ltau le2 le3); + n1_e1, if_cond_lift ltau le2 le3 target_e1, n2_e1 + end else (1, le', 0) | D.EApp de1 de2 dtau_arg -> let le1 = translate_exp de1 in let le2 = translate_exp de2 in let ltau_arg = translate_ty dtau_arg in if not (D.is_value de1) then begin - let de1' = Some?.v (D.step de1) in - let le1' = translate_exp de1' in - let n1_e1, target_e1, n2_e1 = translation_correctness_step de1 (D.TArrow dtau_arg dtau) in - assert(take_l_steps (L.TArrow ltau_arg ltau) le1 n1_e1 == Some target_e1); - assert(take_l_steps (L.TArrow ltau_arg ltau) le1' n2_e1 == Some target_e1); - lift_multiple_l_steps (L.TArrow ltau_arg ltau) ltau le1 target_e1 n1_e1 - (app_f_lift ltau_arg ltau le2); - lift_multiple_l_steps (L.TArrow ltau_arg ltau) ltau le1' target_e1 n2_e1 - (app_f_lift ltau_arg ltau le2); - n1_e1, app_f_lift ltau_arg ltau le2 target_e1, n2_e1 + let de1' = Some?.v (D.step de1) in + let le1' = translate_exp de1' in + let n1_e1, target_e1, n2_e1 = translation_correctness_step de1 (D.TArrow dtau_arg dtau) in + assert(take_l_steps (L.TArrow ltau_arg ltau) le1 n1_e1 == Some target_e1); + assert(take_l_steps (L.TArrow ltau_arg ltau) le1' n2_e1 == Some target_e1); + lift_multiple_l_steps (L.TArrow ltau_arg ltau) ltau le1 target_e1 n1_e1 + (app_f_lift ltau_arg ltau le2); + lift_multiple_l_steps (L.TArrow ltau_arg ltau) ltau le1' target_e1 n2_e1 + (app_f_lift ltau_arg ltau le2); + n1_e1, app_f_lift ltau_arg ltau le2 target_e1, n2_e1 end else begin match de1 with | D.ELit D.LConflictError -> 1, le', 0 | D.ELit D.LEmptyError -> 1, le', 0 @@ -924,10 +968,61 @@ let rec translation_correctness_step (de: D.exp) (dtau: D.ty) | D.EDefault dexceptions djust dcons dtau' -> if dtau' <> dtau then 0, le', 0 else begin match D.step_exceptions de dexceptions djust dcons dtau with - | Some _ -> + | D.SomeStep _ -> translation_correctness_exceptions_step de dexceptions djust dcons dtau (fun df tf -> translation_correctness_step df tf) - | None -> admit() + | D.NoStep -> + let n1_final = + translation_correctness_exceptions_no_exceptions_triggered + de dexceptions djust dcons dtau + in + let ltau = translate_ty dtau in + let ljust = translate_exp djust in + let lcons = translate_exp dcons in + let l_err = L.ELit (L.LError L.EmptyError) in + assert(take_l_steps ltau le n1_final = Some (final_default_subexp ltau ljust lcons)); + if not (D.is_value djust) then begin + let djust' = Some?.v (D.step djust) in + D.preservation djust D.TBool; + translation_preserves_empty_typ djust D.TBool; + translation_preserves_empty_typ dcons dtau; + translation_preserves_empty_typ djust' D.TBool; + let ljust' : typed_l_exp L.TBool = translate_exp djust' in + let n1_just, target_just, n2_just = translation_correctness_step djust D.TBool in + assert(take_l_steps L.TBool ljust n1_just == Some target_just); + assert(take_l_steps L.TBool ljust' n2_just == Some target_just); + lift_multiple_l_steps L.TBool ltau ljust target_just n1_just + (if_cond_lift ltau lcons l_err); + lift_multiple_l_steps L.TBool ltau ljust' target_just n2_just + (if_cond_lift ltau lcons l_err); + take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final n1_just; + assert(take_l_steps ltau le (n1_final + n1_just) == Some (L.EIf target_just lcons l_err)); + assert(de' == D.EDefault dexceptions djust' dcons dtau); + assume(D.step_exceptions de dexceptions djust dcons dtau == + D.step_exceptions de' dexceptions djust' dcons dtau); + // Should be easy enough, djust does not influence the result + let n2_final = + translation_correctness_exceptions_no_exceptions_triggered + de' dexceptions djust' dcons dtau + in + take_l_steps_transitive ltau le' (final_default_subexp ltau ljust' lcons) n2_final n2_just; + n1_final + n1_just, L.EIf target_just lcons l_err, n2_final + n2_just + end else begin + D.is_bool_value_cannot_be_abs D.empty djust; + match djust with + | D.ELit D.LTrue -> + take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final 1; + n1_final + 1, lcons, 0 + | D.ELit D.LFalse -> + take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final 1; + n1_final + 1, l_err, 0 + | D.ELit D.LConflictError -> + take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final 1; + n1_final + 1, L.ELit (L.LError L.ConflictError), 0 + | D.ELit D.LEmptyError -> + take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final 1; + n1_final + 1, l_err, 0 + end end (*** Wrap-up theorem *)