Skip to content

Commit 4340efd

Browse files
jihgfeeineol
jihgfee
authored and
ineol
committed
Added remaining socket lemmas
1 parent a9a31fd commit 4340efd

File tree

1 file changed

+217
-101
lines changed

1 file changed

+217
-101
lines changed

‎fairneris/aneris_lang/lifting.v‎

Lines changed: 217 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -640,121 +640,237 @@ Section primitive_laws.
640640
iSplit; [|done]. by iApply "HΦ".
641641
Qed.
642642

643-
Lemma wp_send φ mbody (is_dup : bool) sh skt a to k E
644-
ζ R T
645-
(Φ : (aneris_expr → option (action aneris_lang) → iProp Σ)) :
646-
let msg := mkMessage a to mbody in
647-
saddress skt = Some a →
643+
Lemma wp_new_socket ip s E ζ (Φ : aneris_expr → option (action aneris_lang) → iProp Σ) :
644+
▷ is_node ip -∗
645+
(∀ sh, sh ↪[ip] (mkSocket None true) -∗ Φ (mkVal ip (LitV (LitSocket sh))) None) -∗
646+
sswp s E ζ (mkExpr ip (NewSocket #())) Φ.
647+
Proof.
648+
iIntros "Hn HΦ".
649+
rewrite /sswp.
650+
iSplit; [done|].
651+
iIntros (ex atr K tp1 tp2 σ Hexvalid Hlocale Hex) "([Hσ Hauth] & [% Hm])".
652+
iMod "Hn".
653+
rewrite (last_eq_trace_ends_in _ _ Hex).
654+
iDestruct (is_node_valid_sockets with "Hσ Hn") as (?) "%".
655+
iApply fupd_mask_intro; [set_solver|]. iIntros "Hclose".
656+
iSplitR; [iPureIntro; eauto|].
657+
{ destruct s; [|done]. do 4 eexists. eapply head_prim_step.
658+
eapply SocketStepS; eauto.
659+
apply newsocket_fresh. }
660+
iIntros (α v2 σ2 efs Hstep).
661+
apply head_reducible_prim_step in Hstep; last first.
662+
{ do 4 eexists. eapply SocketStepS; eauto.
663+
apply newsocket_fresh. }
664+
pose proof (conj Hstep I) as Hstep'.
665+
inv_head_step.
666+
destruct Hstep' as [Hstep' _].
667+
iApply step_fupdN_intro; [done|].
668+
iIntros "!>!>".
669+
set (sock := {| saddress := None;
670+
sblock := true |}).
671+
iMod (aneris_state_interp_alloc_socket sock with "Hn Hσ")
672+
as "[Hσ Hsh]"; try done.
673+
iModIntro. iIntros "!>".
674+
iMod (steps_auth_update _ (S (trace_length ex)) with "Hauth")
675+
as "[Hauth _]"; [by eauto|].
676+
iMod "Hclose" as "_".
677+
iModIntro. iFrame. simpl.
678+
rewrite (last_eq_trace_ends_in _ _ Hex). simpl.
679+
rewrite -message_history_evolution_new_socket; [|done|done].
680+
iFrame.
681+
iSplitL "Hm".
682+
{ iExists ex.
683+
iSplit.
684+
{ iPureIntro. simpl. by eexists _. }
685+
rewrite /aneris_state_interp_δ. rewrite Hex. iFrame.
686+
iSplit; [|done].
687+
iPureIntro.
688+
eapply (locale_step_atomic _ _ _ _ _ _ _ []); try done.
689+
{ by rewrite right_id_L. }
690+
apply fill_step.
691+
eapply head_prim_step. simpl. done. }
692+
iSplit; [|done]. by iApply "HΦ".
693+
Qed.
694+
695+
(* Lemma wp_socketbind A E ζ sh skt k a : *)
696+
(* saddress skt = None → *)
697+
(* {{{ ▷ free_ports (ip_of_address a) {[port_of_address a]} ∗ *)
698+
(* ▷ sh ↪[ip_of_address a] skt }}} *)
699+
(* (mkExpr (ip_of_address a) *)
700+
(* (SocketBind (Val $ LitV $ LitSocket sh) *)
701+
(* (Val $ LitV $ LitSocketAddress a))) @ k; ζ; E *)
702+
(* {{{ RET (mkVal (ip_of_address a) #0); *)
703+
(* sh ↪[ip_of_address a] (skt<| saddress := Some a |>) }}}. *)
704+
705+
Lemma wp_socketbind s E ζ sh skt a (Φ : aneris_expr → option (action aneris_lang) → iProp Σ) :
706+
saddress skt = None →
707+
▷ free_ports (ip_of_address a) {[port_of_address a]} -∗
648708
▷ sh ↪[ip_of_address a] skt -∗
649-
▷ a ⤳ (R, T) -∗
650-
▷ to ⤇ φ -∗
651-
(if is_dup then ⌜msg ∈ T⌝ else ▷ φ msg) -∗
652-
(sh ↪[ip_of_address a] skt -∗ a ⤳ (R, {[ msg ]} ∪ T) -∗
653-
Φ (mkVal (ip_of_address a) #(String.length mbody)) (Some (Send msg))) -∗
654-
sswp k E ζ
655-
(mkExpr (ip_of_address a)
656-
(SendTo (Val $ LitV $ LitSocket sh) #mbody #to)) Φ.
709+
(sh ↪[ip_of_address a] (skt<| saddress := Some a |>) -∗ Φ (mkVal (ip_of_address a) #0) None) -∗
710+
sswp s E ζ (mkExpr (ip_of_address a)
711+
(SocketBind (Val $ LitV $ LitSocket sh)
712+
(Val $ LitV $ LitSocketAddress a))) Φ.
657713
Proof.
658-
iIntros (msg Hskt) "Hsh Hrt Hφ Hmsg HΦ".
659-
iAssert (▷ socket_address_group_own {[a]})%I as "#Ha".
660-
{ iDestruct "Hrt" as "[(%send & %recv & _ & _ & _ & $ & _) _]". }
661-
iAssert (▷ socket_address_group_own {[to]})%I as "#Hto".
662-
{ iNext. by iDestruct "Hφ" as (γ) "[H _]". }
663-
iDestruct "Hrt" as "[Hrt Hown]".
714+
iIntros (?) "Hp Hsh HΦ".
664715
rewrite /sswp.
665716
iSplit; [done|].
666-
iIntros (ex atr K tp1 tp2 σ Hexvalid Hlocale Hex) "[[Hσ Hauth] [%Hvalid Hm]]".
667-
iMod (steps_auth_update_S with "Hauth") as "Hauth".
668-
iMod "Hsh". iMod "Hrt".
717+
iIntros (ex atr K tp1 tp2 σ Hexvalid Hlocale Hex) "([Hσ Hauth] & [% Hm])".
718+
iMod "Hp".
719+
iMod "Hsh".
669720
rewrite (last_eq_trace_ends_in _ _ Hex).
670-
iDestruct (aneris_state_interp_network_sockets_coh_valid with "Hσ") as %Hcoh.
671721
iDestruct (aneris_state_interp_socket_valid with "Hσ Hsh")
672722
as (Sn r) "[%HSn (%Hr & %Hreset)]".
673-
iApply fupd_mask_intro; [set_solver|].
674-
iIntros "Hclose".
675-
iSplitR.
676-
{ destruct k; [|done].
677-
iPureIntro; do 4 eexists. eapply head_prim_step. eapply SocketStepS; eauto.
678-
by econstructor; naive_solver. }
679-
iIntros (α e2 σ2 efs Hstep).
723+
iDestruct (aneris_state_interp_free_ports_valid with "Hσ Hp") as "%HP".
724+
{ apply HSn. }
725+
iApply fupd_mask_intro; [set_solver|]. iIntros "Hclose".
726+
iSplitR; [iPureIntro; eauto|].
727+
{ destruct s; [|done]. do 4 eexists. eapply head_prim_step.
728+
eapply SocketStepS; eauto.
729+
econstructor; naive_solver. }
730+
iIntros (α v2 σ2 efs Hstep).
680731
apply head_reducible_prim_step in Hstep; last first.
681-
{ do 4 eexists. eapply SocketStepS; eauto. by econstructor. }
732+
{ do 4 eexists. eapply SocketStepS; eauto.
733+
econstructor; naive_solver. }
682734
pose proof (conj Hstep I) as Hstep'.
683735
inv_head_step.
684736
destruct Hstep' as [Hstep' _].
685737
iApply step_fupdN_intro; [done|].
686-
destruct is_dup; last first.
687-
- iIntros "!>!>".
688-
iModIntro.
689-
iIntros "!>".
690-
iMod (aneris_state_interp_send sh a {[a]} to {[to]} _ _ skt
691-
with "[] [] [$Hsh] [$Hrt] [Hφ] [Hmsg] [$Hσ]")
692-
as "(%Hmhe & Hσ & Hsh & Hrt)"; try done.
693-
{ apply message_group_equiv_refl; try set_solver. }
694-
{ iSplit; [|done]. iPureIntro. set_solver. }
695-
{ iSplit; [|done]. iPureIntro. set_solver. }
696-
{ iSplit; [|done]. done. }
697-
iMod "Hclose". iModIntro.
698-
iSplitL "Hσ Hauth Hm".
699-
{ iFrame.
700-
iSplitL "Hσ".
701-
- simpl.
702-
rewrite (last_eq_trace_ends_in _ _ Hex). simpl.
703-
rewrite Hmhe.
704-
simpl.
705-
rewrite insert_id; [|done].
706-
rewrite - /msg.
707-
simpl.
708-
iFrame.
709-
- simpl.
710-
iExists ex.
711-
iSplit.
712-
{ iPureIntro. simpl. by eexists _. }
713-
rewrite /aneris_state_interp_δ. rewrite Hex. iFrame.
714-
iSplit; [|done].
715-
iPureIntro.
716-
eapply (locale_step_atomic _ _ _ _ _ _ _ []); try done.
717-
{ by rewrite right_id_L. }
718-
apply fill_step.
719-
eapply head_prim_step. simpl. done. }
738+
iIntros "!>!>".
739+
iMod (aneris_state_interp_socketbind with "Hσ Hsh Hp")
740+
as "(Hσ & Hsh)"; [set_solver..|].
741+
iModIntro. iIntros "!>".
742+
iMod (steps_auth_update _ (S (trace_length ex)) with "Hauth")
743+
as "[Hauth _]"; [by eauto|].
744+
iMod "Hclose" as "_".
745+
iModIntro. iFrame. simpl.
746+
rewrite (last_eq_trace_ends_in _ _ Hex). simpl.
747+
rewrite -message_history_evolution_socketbind; [|done|done].
748+
iFrame.
749+
iSplitL "Hm".
750+
{ iExists ex.
751+
iSplit.
752+
{ iPureIntro. simpl. by eexists _. }
753+
rewrite /aneris_state_interp_δ. rewrite Hex. iFrame.
720754
iSplit; [|done].
721-
iApply ("HΦ" with "Hsh [$Hrt $Hown]").
722-
- iIntros "!>!>".
723-
iModIntro.
724-
iIntros "!>".
725-
iDestruct "Hmsg" as "%Hmsg".
726-
iMod (aneris_state_interp_send_duplicate sh a {[a]} to {[to]} _ _ skt
727-
with "[] [] [$Hsh] [$Hrt] [$Hσ]")
728-
as "(%Hmhe & Hσ & Hsh & Hrt)"; try done.
729-
{ eexists _. split; [done|].
730-
apply message_group_equiv_refl; try set_solver. }
731-
{ iSplit; [|done]. iPureIntro. set_solver. }
732-
{ iSplit; [|done]. iPureIntro. set_solver. }
733-
iMod "Hclose". iModIntro.
734-
iSplitL "Hσ Hauth Hm".
735-
{ iFrame.
736-
iSplitL "Hσ".
737-
- simpl.
738-
rewrite (last_eq_trace_ends_in _ _ Hex). simpl.
739-
rewrite Hmhe.
740-
simpl.
741-
rewrite insert_id; [|done].
742-
rewrite - /msg.
743-
simpl.
744-
iFrame.
745-
- simpl.
746-
iExists ex.
747-
iSplit.
748-
{ iPureIntro. simpl. by eexists _. }
749-
rewrite /aneris_state_interp_δ. rewrite Hex. iFrame.
750-
iSplit; [|done].
751-
iPureIntro.
752-
eapply (locale_step_atomic _ _ _ _ _ _ _ []); try done.
753-
{ by rewrite right_id_L. }
754-
apply fill_step.
755-
eapply head_prim_step. simpl. done. }
755+
iPureIntro.
756+
eapply (locale_step_atomic _ _ _ _ _ _ _ []); try done.
757+
{ by rewrite right_id_L. }
758+
apply fill_step.
759+
eapply head_prim_step. simpl. done. }
760+
iSplit; [|done]. by iApply "HΦ".
761+
Qed.
762+
763+
Lemma wp_rcvtimeo_block s E ζ sh skt a
764+
(Φ : aneris_expr → option (action aneris_lang) → iProp Σ) :
765+
let ip := ip_of_address a in
766+
saddress skt = Some a →
767+
▷ sh ↪[ip] skt -∗
768+
(sh ↪[ip] skt<|sblock := true|> -∗ Φ (mkVal ip #()) None) -∗
769+
sswp s E ζ (mkExpr ip (SetReceiveTimeout
770+
(Val $ LitV $ LitSocket sh)
771+
(Val $ LitV $ LitInt 0)
772+
(Val $ LitV $ LitInt 0))) Φ.
773+
Proof.
774+
iIntros (??) "Hsh HΦ".
775+
rewrite /sswp.
776+
iSplit; [done|].
777+
iIntros (ex atr K tp1 tp2 σ Hexvalid Hlocale Hex) "([Hσ Hauth] & [% Hm])".
778+
iMod "Hsh".
779+
rewrite (last_eq_trace_ends_in _ _ Hex).
780+
iDestruct (aneris_state_interp_socket_valid with "Hσ Hsh")
781+
as (Sn r) "[%HSn (%Hr & %Hreset)]".
782+
iApply fupd_mask_intro; [set_solver|]. iIntros "Hclose".
783+
iSplitR; [iPureIntro; eauto|].
784+
{ destruct s; [|done]. do 4 eexists. eapply head_prim_step.
785+
eapply SocketStepS; eauto.
786+
econstructor; naive_solver. }
787+
iIntros (α v2 σ2 efs Hstep).
788+
apply head_reducible_prim_step in Hstep; last first.
789+
{ do 4 eexists. eapply SocketStepS; eauto.
790+
econstructor; naive_solver. }
791+
pose proof (conj Hstep I) as Hstep'.
792+
inv_head_step; first by lia.
793+
destruct Hstep' as [Hstep' _].
794+
iApply step_fupdN_intro; [done|].
795+
iIntros "!>!>".
796+
iMod (aneris_state_interp_sblock_update with "Hσ Hsh") as "(Hσ&Hsh)"; eauto.
797+
iModIntro. iIntros "!>".
798+
iMod (steps_auth_update _ (S (trace_length ex)) with "Hauth")
799+
as "[Hauth _]"; [by eauto|].
800+
iMod "Hclose" as "_".
801+
iModIntro. iFrame. simpl.
802+
rewrite (last_eq_trace_ends_in _ _ Hex). simpl.
803+
rewrite -message_history_evolution_update_sblock; [|done|done].
804+
iFrame.
805+
iSplitL "Hm".
806+
{ iExists ex.
807+
iSplit.
808+
{ iPureIntro. simpl. by eexists _. }
809+
rewrite /aneris_state_interp_δ. rewrite Hex. iFrame.
810+
iSplit; [|done].
811+
iPureIntro.
812+
eapply (locale_step_atomic _ _ _ _ _ _ _ []); try done.
813+
{ by rewrite right_id_L. }
814+
apply fill_step.
815+
eapply head_prim_step. simpl. done. }
816+
iSplit; [|done]. by iApply "HΦ".
817+
Qed.
818+
819+
Lemma wp_rcvtimeo_ublock s E ζ sh skt a n1 n2
820+
(Φ : aneris_expr → option (action aneris_lang) → iProp Σ) :
821+
let ip := ip_of_address a in
822+
saddress skt = Some a →
823+
(0 ≤ n1 ∧ 0 <= n2 ∧ 0 < n1 + n2)%Z →
824+
▷ sh ↪[ip] skt -∗
825+
(sh ↪[ip] skt<|sblock := false|> -∗ Φ (mkVal ip #()) None) -∗
826+
sswp s E ζ (mkExpr ip (SetReceiveTimeout
827+
(Val $ LitV $ LitSocket sh)
828+
(Val $ LitV $ LitInt n1)
829+
(Val $ LitV $ LitInt n2))) Φ.
830+
Proof.
831+
iIntros (???) "Hsh HΦ".
832+
rewrite /sswp.
833+
iSplit; [done|].
834+
iIntros (ex atr K tp1 tp2 σ Hexvalid Hlocale Hex) "([Hσ Hauth] & [% Hm])".
835+
iMod "Hsh".
836+
rewrite (last_eq_trace_ends_in _ _ Hex).
837+
iDestruct (aneris_state_interp_socket_valid with "Hσ Hsh")
838+
as (Sn r) "[%HSn (%Hr & %Hreset)]".
839+
iApply fupd_mask_intro; [set_solver|]. iIntros "Hclose".
840+
iSplitR; [iPureIntro; eauto|].
841+
{ destruct s; [|done]. do 4 eexists. eapply head_prim_step.
842+
eapply SocketStepS; eauto.
843+
econstructor; naive_solver. }
844+
iIntros (α v2 σ2 efs Hstep).
845+
apply head_reducible_prim_step in Hstep; last first.
846+
{ do 4 eexists. eapply SocketStepS; eauto.
847+
econstructor; naive_solver. }
848+
pose proof (conj Hstep I) as Hstep'.
849+
inv_head_step; last by lia.
850+
destruct Hstep' as [Hstep' _].
851+
iApply step_fupdN_intro; [done|].
852+
iIntros "!>!>".
853+
iMod (aneris_state_interp_sblock_update with "Hσ Hsh") as "(Hσ&Hsh)"; eauto.
854+
iModIntro. iIntros "!>".
855+
iMod (steps_auth_update _ (S (trace_length ex)) with "Hauth")
856+
as "[Hauth _]"; [by eauto|].
857+
iMod "Hclose" as "_".
858+
iModIntro. iFrame. simpl.
859+
rewrite (last_eq_trace_ends_in _ _ Hex). simpl.
860+
rewrite -message_history_evolution_update_sblock; [|done|done].
861+
iFrame.
862+
iSplitL "Hm".
863+
{ iExists ex.
864+
iSplit.
865+
{ iPureIntro. simpl. by eexists _. }
866+
rewrite /aneris_state_interp_δ. rewrite Hex. iFrame.
756867
iSplit; [|done].
757-
iApply ("HΦ" with "Hsh [$Hrt $Hown]").
868+
iPureIntro.
869+
eapply (locale_step_atomic _ _ _ _ _ _ _ []); try done.
870+
{ by rewrite right_id_L. }
871+
apply fill_step.
872+
eapply head_prim_step. simpl. done. }
873+
iSplit; [|done]. by iApply "HΦ".
758874
Qed.
759875

760876
Lemma wp_recv

0 commit comments

Comments
 (0)