proposition: Lemma head_grant_state_unlock : forall st tr c t, step_async_star step_async_init st tr -> queue (nwState st Server) = c :: t -> (In (mkPacket Server (Client c) Locked) (nwPackets st)) \/ (held (nwState st (Client c)) = true) \/ (In (mkPacket (Client c) Server Unlock) (nwPackets st)).
proof: Proof. Proof using. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. prep_induction H. induction H; intros; subst. - discriminate. - match goal with | [ H : step_async _ _ _ |- _ ] => invcs H end; unlabeled_unfold; unfold lb_net_handlers, lb_input_handlers in *; simpl in *; monad_unfold; repeat break_let; repeat find_inversion. + unfold NetHandler in *. break_match; rewrite_update. * find_apply_lem_hyp ClientNetHandler_cases. intuition. -- subst. rewrite update_nop_ext. find_apply_lem_hyp IHrefl_trans_n1_trace; auto; [idtac]. repeat find_rewrite. in_crush_tac (intuition auto with datatypes). discriminate. -- subst. find_apply_lem_hyp refl_trans_n1_1n_trace. find_apply_lem_hyp reachable_intro. match goal with | [ H : reachable _ _ _ |- _ ] => let H' := fresh H in pose H as H'; eapply locks_correct_locked_invariant with (p := p) in H'; [| now repeat find_rewrite; intuition auto with datatypes]; eapply locks_correct_locked_at_head in H'; eauto end. unfold at_head_of_queue in *. break_exists. find_rewrite. find_inversion. rewrite_update. auto. * find_apply_lem_hyp ServerNetHandler_cases. intuition. -- break_exists. intuition. ++ subst. repeat find_rewrite. simpl in *. find_inversion. auto. ++ subst. repeat find_rewrite. destruct (queue (nwState x' Server)); try congruence. simpl in *. find_inversion. do 2 insterU IHrefl_trans_n1_trace. repeat conclude_using eauto. intuition. ** in_crush_tac (intuition auto with datatypes). discriminate. ** in_crush_tac (intuition auto with datatypes). discriminate. -- congruence. -- break_exists. intuition. subst. simpl. repeat find_rewrite. find_inversion. auto. -- subst. simpl. find_apply_hyp_hyp. intuition. ++ repeat find_rewrite. in_crush_tac (intuition auto with datatypes). discriminate. ++ repeat find_rewrite. in_crush_tac (intuition auto with datatypes). + find_apply_lem_hyp InputHandler_cases. intuition. * break_exists. break_and. subst. rewrite_update. find_apply_hyp_hyp. intuition auto with datatypes. -- subst. rewrite update_nop_ext. auto. -- find_apply_lem_hyp refl_trans_n1_1n_trace. find_apply_lem_hyp reachable_intro. match goal with | [ H : reachable _ _ _ |- _ ] => pose H as Hmutex; eapply mutual_exclusion_invariant in Hmutex end. unfold mutual_exclusion in *. assert (c = x) by auto. clear Hmutex. subst. simpl. auto. -- subst. rewrite_update. auto. * subst. simpl. rewrite update_nop_ext in *. match goal with | [ H : _ |- _ ] => apply IHrefl_trans_n1_trace in H; auto end. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)