Commit f4e721d4 authored by Michael Sammler's avatar Michael Sammler
Browse files

more proofs

parent b5594236
Pipeline #50046 failed with stage
in 18 minutes and 38 seconds
......@@ -207,22 +207,22 @@ Section uninit.
(* Typing rule for [Return] (used in [theories/typing/automation.v]). *)
Lemma type_return Q e fn ls R:
typed_val_expr e (λ v ty,
foldr (λ (e : (loc * layout)) T, e.1 ◁ₗ uninit e.2 T)
(R v ty)
(zip ls (fn.(f_args) ++ fn.(f_local_vars)).*2)) -
foldr (λ (e : (loc * layout)) T, e.1 ◁ₗ uninit e.2 T)
(R v ty)
(zip ls (fn.(f_args) ++ fn.(f_local_vars)).*2)) -
typed_stmt (Return e) fn ls R Q.
Proof.
iIntros "He" (Hls). wps_bind. iApply "He".
iIntros (v ty) "Hv HR". iApply wps_return.
Admitted.
(* iDestruct ("HR" with "Hv") as (x) "[? HR]". iExists _. iFrame. *)
(* move: Hls. move: (f_args fn ++ f_local_vars fn) => lys {fn} Hlys. *)
(* iInduction ls as [|l ls] "IH" forall (lys Hlys); *)
(* destruct lys as [|ly lys]=> //; csimpl in *; simplify_eq; *)
(* [rewrite right_id; by iFrame|]. *)
(* iDestruct "HR" as "[Hl HR]". rewrite /ty_own/=. iDestruct "Hl" as (????) "Hl". *)
(* iDestruct ("IH" with "[//] HR") as "[$ $]". iExists _. by iFrame. *)
(* Qed. *)
rewrite /typed_stmt_post_cond. move: Hls. move: (f_args fn ++ f_local_vars fn) => lys {fn} Hlys.
iInduction ls as [|l ls] "IH" forall (lys Hlys); destruct lys as [|ly lys]=> //; csimpl in *; simplify_eq.
{ iExists _. iFrame. }
iDestruct "HR" as "[Hl HR]".
iDestruct ("IH" with "[//] Hv HR") as (ty') "[?[??]]".
iExists _. iFrame.
rewrite /ty_own/=. iDestruct "Hl" as (????) "Hl".
iExists _. by iFrame.
Qed.
Lemma annot_to_uninit l ty T `{!Movable ty}:
( v, v ◁ᵥ ty - l ◁ₗ uninit ty.(ty_layout) - T) -
......
......@@ -231,55 +231,33 @@ Section inline_function.
(zip vl tys)
[])
- typed_call v (v ◁ᵥ l @ inline_function_ptr fn) vl tys T.
Proof. Admitted.
(*
iIntros "(%x&Hvl&HPa&Hr) (%fn&->&He&Hfn)" (Φ) "HΦ".
iDestruct ("Hfn" $! x) as "[>%Hl #Hfn]".
Proof.
iIntros "[%Hl HT] (->&Hfn) Htys" (Φ) "HΦ".
iAssert Forall2 has_layout_val vl (f_args fn).*2%I as %Hall. {
iClear "Hfn HPa Hr".
move: Hl. move: (fp_atys (fp x)) => atys Hl.
iInduction (fn.(f_args)) as [|[??]] "IH" forall (vl atys Hl).
iClear "Hfn HT HΦ".
iInduction (fn.(f_args)) as [|[??]] "IH" forall (vl tys Hl).
{ move: Hl => /Forall2_nil_inv_r ->. destruct vl => //=. }
move: Hl. intros (?&?&Heq&?&->)%Forall2_cons_inv_r.
destruct vl => //=. iDestruct "Hvl" as "[Hv Hvl]".
iDestruct ("IH" with "[//] Hvl He HΦ") as %?.
destruct vl => //=. iDestruct "Htys" as "[Hv Hvl]".
iDestruct ("IH" with "[//] Hvl") as %?.
iDestruct (ty_size_eq with "Hv") as %?.
iPureIntro. constructor => //. by rewrite -Heq.
}
iApply (wp_call with "He") => //. { by apply val_to_of_loc. }
iApply (wp_call with "Hfn") => //. { by apply val_to_of_loc. }
iIntros "!#" (lsa lsv Hly) "Ha Hv".
iDestruct (big_sepL2_length with "Ha") as %Hlen1.
iDestruct (big_sepL2_length with "Hv") as %Hlen2.
iDestruct (big_sepL2_length with "Hvl") as %Hlen3.
have [lsa' ?]: (∃ (ls : vec loc (length (fp_atys (fp x)))), lsa = ls) by rewrite -Hlen3 -Hlen1; eexists (list_to_vec _); symmetry; apply vec_to_list_to_vec. subst.
have [lsv' ?]: (∃ (ls : vec loc (length (f_local_vars fn))), lsv = ls) by rewrite -Hlen2; eexists (list_to_vec _); symmetry; apply vec_to_list_to_vec. subst.
iDestruct ("Hfn" $! lsa' lsv') as "#Hm". iClear "Hfn".
iExists _. iSplitR "Hr HΦ" => /=.
- iFrame. iApply ("Hm" with "[-]"). 2:{
iPureIntro. rewrite !app_length. f_equal => //. rewrite Hlen1 Hlen3. by eapply Forall2_length.
} iClear "Hm". iFrame.
move: Hlen1 Hly. move: (lsa' : list _) => lsa'' Hlen1 Hly. clear lsa' Hall.
move: Hlen3 Hl. move: (fp_atys (fp x)) => atys Hlen3 Hl.
move: Hly Hl. move: (f_args fn) => alys Hly Hl.
iInduction (vl) as [|v vl] "IH" forall (atys lsa'' alys Hlen1 Hly Hlen3 Hl).
{ destruct atys, lsa'' => //. iSplitR => //. iApply (big_sepL2_mono with "Hv").
iIntros (?????) => /=. iDestruct 1 as (??) "[%?]".
iExists _. iFrame. by rewrite Forall_forall. }
destruct atys, lsa'' => //.
move: Hl => /(Forall2_cons_inv_l _ _)[[??][?[?[??]]]]; simplify_eq. csimpl in *.
move: Hly => /(Forall2_cons_inv _ _ _ _)[??].
iDestruct "Hvl" as "[Hvl ?]".
iDestruct "Ha" as "[Ha ?]".
iDestruct (ty_ref with "[] Ha Hvl") as "$". done.
by iApply ("IH" with "[] [] [] [] [$] [$]").
- iIntros (v). iDestruct 1 as (x') "[Hv [Hls HPr]]".
iDestruct (big_sepL2_app_inv with "Hls") as "[$ $]".
{ rewrite Hlen1 Hlen3. left. by eapply Forall2_length. }
iApply ("HΦ" with "Hv").
by iApply ("Hr" with "HPr").
Qed.
*)
(* iDestruct (big_sepL2_length with "Ha") as %Hlen1. *)
(* iDestruct (big_sepL2_length with "Hv") as %Hlen2. *)
(* iDestruct (big_sepL2_length with "Htys") as %Hlen3. *)
move: Hl Hall Hly. move: {1 2 3}(f_args fn) => alys Hl Hall Hly.
iInduction vl as [|v vl] "IH" forall (tys lsa alys Hly Hl Hall) => /=. 2: {
admit.
}
move: {1 2}(f_local_vars fn) => vlys.
iInduction lsv as [|lv lsv] "IH" forall (vlys) => /=. 2: {
admit.
}
simpl.
Admitted.
Global Instance type_call_inline_fnptr_inst l v vl tys fn :
TypedCallVal v (l @ inline_function_ptr fn) vl tys :=
λ T, i2p (type_call_inline_fnptr l v vl tys T fn).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment