Library mcertikos.objects.dev.ObjX86Proof

Require Import Coqlib.
Require Import Maps.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Constant.
Require Import OracleInstances.
Require Import ObjInterruptController.
Require Import ObjInterruptDriver.
Require Import ObjConsole.
Require Import ObjX86.
Require Import ObjInterruptManagement.

Require Import FutureTactic.
Require Import CommonTactic.
Require Import XOmega.

Section OBJ_X86Proof.
  Section SeparationProof.

    Variables T1 T2: Type.

    Variable f1: T1 → T1.
    Variable f2: T2 → T2.

    Variable f: T1 → T2 → (T1 × T2).

    Variable f1´: T1 → T1.

    Hypothesis f1_spec: ∀ x: T1, f1 x = f1´ x.
    Hypothesis f2_same: ∀ x: T2, f2 x = x.
    Hypothesis f_spec: ∀ x y, f x y = (f1 x, f2 y).

    Theorem f_simpl:
      ∀ x y, f x y = (f1´ x, y).
    Proof.
      firstorder.
    Qed.
  End SeparationProof.

  Section Save_Restore_Left_Inversion.

    Section WITH_RDATA.

      Variable d: RData.

      Hypothesis valid_idle_tf:
        ∀ n, nth n (tf d) tf_init_d = tf_init_d.

      Hypothesis valid_tf_length:
        length (tf d) = MAX_IRQ_NUM.

      Lemma save_restore_left_inverse_abd:
        ∀ rs rs´ d´ d´´,
          in_intr d = false →
          save_context_spec rs d = d´ →
          restore_context_spec d´ = (rs´, d´´) →
          d = d´´.
      Proof.
        intros rs rs´ d´ d´´ Hintr Hsave Hres.
        functional inversion Hsave. functional inversion Hres; subst.
        rewrite <- H2 in H1.
        simpl in H1.
        eapply app_eq_nil in H1.
        destruct H1.
        inv H0.
        simpl.
        rewrite removelast_app.
        simpl.
        rewrite app_nil_r.
        destruct d; simpl.
        reflexivity.
        intro contra; inv contra.
      Qed.

      Lemma save_restore_left_inverse_rs:
        ∀ rs rs´ d´ d´´,
          in_intr d = false →
          save_context_spec rs d = d´ →
          restore_context_spec d´ = (rs´, d´´) →
          rs = rs´.
      Proof.
        intros rs rs´ d´ d´´ Hintr Hsave Hres.
        functional inversion Hsave. functional inversion Hres; subst.
        rewrite <- H2 in H1.
        simpl in H1.
        eapply app_eq_nil in H1.
        destruct H1.
        inv H0.
        simpl.
        rewrite last_concat.
        reflexivity.
        intro contra; inv contra.
      Qed.

      Lemma save_restore_basic_transparent:
        ∀ (rs rs´: regset) (d1 d2 d´: RData)
          (spec: RData → option (RData)),
          in_intr d = false →
          (∀ dx dy, spec dx = Some (dy) → tf dy = tf dx) →
          (∀ dx dy x, spec dx = Some (dy) → spec (dx {tf: x}) = Some (dy {tf: x})) →
          save_context_spec rs d = d1 →
          spec d1 = Some (d2) →
          restore_context_spec d2 = (rs´, d´) →
          spec d = Some (d´).
      Proof.
        intros rs rs´ d1 d2 d´ spec Hintr Hisotf Hnonint Hsave Hspec Hres.
        functional inversion Hsave. functional inversion Hres; subst.
        eapply Hisotf in Hspec.
        simpl in Hspec.
        rewrite H1 in Hspec.
        symmetry in Hspec.
        eapply app_eq_nil in Hspec.
        destruct Hspec.
        inv H0.
        generalize (Hisotf _ _ Hspec). intros Htf21.
        generalize (Hnonint _ _ (removelast (tf d2)) Hspec).
        intros Hd12.
        rewrite <- Hd12.
        rewrite Htf21.
        simpl.
        rewrite removelast_app.
        simpl.
        rewrite app_nil_r.
        destruct d; simpl; reflexivity.
        intro contra; inv contra.
      Qed.

    Lemma save_restore_basic_preserves_rs:
      ∀ (rs rs´: regset) (d1 d2 d´: RData)
        (spec: RData → option (RData)),
        in_intr d = false →
        (∀ dx dy, spec dx = Some (dy) → tf dy = tf dx) →
        save_context_spec rs d = d1 →
        spec d1 = Some (d2) →
        restore_context_spec d2 = (rs´, d´) →
        rs = rs´.
    Proof.
      intros rs rs´ d1 d2 d´ spec Hintr Hisotf Hsave Hspec Hres.
      functional inversion Hsave. functional inversion Hres; subst.
      eapply Hisotf in Hspec.
      simpl in Hspec.
      rewrite H1 in Hspec.
      symmetry in Hspec.
      eapply app_eq_nil in Hspec.
      destruct Hspec.
      inv H0.
      generalize (Hisotf _ _ Hspec). intros Htf21.
      rewrite Htf21.
      simpl.
      rewrite last_concat.
      reflexivity.
      intro contra; inv contra.
    Qed.

    Lemma save_restore_basic_spec:
      ∀ (rs rs´: regset) (d1 d2 d´: RData)
        (spec: RData → option (RData)),
        in_intr d = false →
        (∀ dx dy, spec dx = Some (dy) → tf dy = tf dx) →
        (∀ dx dy x, spec dx = Some (dy) → spec (dx {tf: x}) = Some (dy {tf: x})) →
        save_context_spec rs d = d1 →
        spec d1 = Some (d2) →
        restore_context_spec d2 = (rs´, d´) →
        (spec d = Some (d´) ∧ rs = rs´).
    Proof.
      intros. split.
      eapply save_restore_basic_transparent; eassumption.
      eapply save_restore_basic_preserves_rs; eassumption.
    Qed.

    Section Save_Restore_Basic_Rewrite.

      Variable spec: RData → option (RData).
      Variable spec_outer: regset → RData → option (RData × regset).

      Hypothesis spec_inner_outer_relation:
        ∀ rs rs´ d d1 d2 d´,
          save_context_spec rs d = d1 →
          spec d1 = Some (d2) →
          restore_context_spec d2 = (rs´, d´) →
          spec_outer rs d = Some (d´, rs´).

      Hypothesis inner_spec_does_not_change_tf:
        ∀ dx dy, spec dx = Some (dy) → tf dy = tf dx.

      Hypothesis inner_spec_independent_from_tf:
        ∀ dx dy x, spec dx = Some (dy) → spec (dx {tf: x}) = Some (dy {tf: x}).

      Hypothesis Hin_intr: in_intr d = false.

      Lemma save_restore_basic_rewrite:
        ∀ rs d´,
          spec d = Some d´ →
          spec_outer rs d = Some (d´, rs).
      Proof.
        intros.
        eapply spec_inner_outer_relation. reflexivity.
        unfold save_context_spec. erewrite inner_spec_independent_from_tf. reflexivity. eassumption.
        unfold restore_context_spec.
        simpl.
        case_eq (tf d ++
                    {|
                      tf_regs := rs;
                      tf_trapno := curr_intr_num d;
                      tf_err := 0;
                      tf_esp := rs ESP |} :: nil); intros.
        eapply app_eq_nil in H0.
        destruct H0.
        inv H1.
        rewrite <- H0; simpl.
        rewrite last_concat.
        rewrite removelast_app.
        simpl.
        rewrite app_nil_r.
        erewrite <- inner_spec_does_not_change_tf by eassumption.
        destruct d´; simpl; reflexivity.
        intro contra; inv contra.
        intro contra; inv contra.
      Qed.

    End Save_Restore_Basic_Rewrite.


    Lemma save_restore_rv_transparent:
      ∀ {T} (rs rs´: regset) (d1 d2 d´: RData)
        (spec: RData → option (RData × T)) (rv: T),
        in_intr d = false →
        (∀ dx dy rv, spec dx = Some (dy, rv) → tf dy = tf dx) →
        (∀ dx dy rv x, spec dx = Some (dy, rv) → spec (dx {tf: x}) = Some (dy {tf: x}, rv)) →
        save_context_spec rs d = d1 →
        spec d1 = Some (d2, rv) →
        restore_context_spec d2 = (rs´, d´) →
        spec d = Some (d´, rv).
    Proof.
      intros T rs rs´ d1 d2 d´ spec r Hintr Hisotf Hnonint Hsave Hspec Hres.
      functional inversion Hsave. functional inversion Hres; subst.
      eapply Hisotf in Hspec.
      simpl in Hspec.
      rewrite H1 in Hspec.
      symmetry in Hspec.
      eapply app_eq_nil in Hspec.
      destruct Hspec.
      inv H0.
      generalize (Hisotf _ _ _ Hspec). intros Htf21.
      generalize (Hnonint _ _ _ (removelast (tf d2)) Hspec).
      intros Hd12.
      rewrite <- Hd12.
      rewrite Htf21.
      simpl.
      rewrite removelast_app.
      simpl.
      rewrite app_nil_r.
      destruct d; simpl; reflexivity.
      intro contra; inv contra.
    Qed.

    Lemma save_restore_rv_preserves_rs:
      ∀ {T} (rs rs´: regset) (d1 d2 d´: RData)
        (spec: RData → option (RData × T)) (rv: T),
        in_intr d = false →
        (∀ dx dy rv, spec dx = Some (dy, rv) → tf dy = tf dx) →
        save_context_spec rs d = d1 →
        spec d1 = Some (d2, rv) →
        restore_context_spec d2 = (rs´, d´) →
        rs = rs´.
    Proof.
      intros T rs rs´ d1 d2 d´ spec r Hintr Hisotf Hsave Hspec Hres.
      functional inversion Hsave. functional inversion Hres; subst.
      eapply Hisotf in Hspec.
      simpl in Hspec.
      rewrite H1 in Hspec.
      symmetry in Hspec.
      eapply app_eq_nil in Hspec.
      destruct Hspec.
      inv H0.
      generalize (Hisotf _ _ _ Hspec). intros Htf21.
      rewrite Htf21.
      simpl.
      rewrite last_concat.
      reflexivity.
      intro contra; inv contra.
    Qed.

    Lemma save_restore_rv_spec:
      ∀ {T} (rs rs´: regset) (d1 d2 d´: RData)
        (spec: RData → option (RData × T)) (rv: T),
        in_intr d = false →
        (∀ dx dy rv, spec dx = Some (dy, rv) → tf dy = tf dx) →
        (∀ dx dy rv x, spec dx = Some (dy, rv) → spec (dx {tf: x}) = Some (dy {tf: x}, rv)) →
        save_context_spec rs d = d1 →
        spec d1 = Some (d2, rv) →
        restore_context_spec d2 = (rs´, d´) →
        (spec d = Some (d´, rv) ∧ rs = rs´).
    Proof.
      intros. split.
      eapply save_restore_rv_transparent; eassumption.
      eapply save_restore_rv_preserves_rs; eassumption.
    Qed.

    End WITH_RDATA.

  End Save_Restore_Left_Inversion.

  Lemma serial_intr_handler_asm_decompose:
    ∀ d d1 d2 d3 d4 d5 d´ rs rs´,
      ikern d = true →
      ihost d = true →
      init d = true →
      in_intr d = true →
      save_context_spec rs d = d1 →
      d1 {ioapic / s / IoApicEnables [4%nat]: false} {intr_flag: true} = d2 →
      lapic_eoi_spec d2 = Some d3 →
      cons_intr_aux d3 = Some d4 →
      d4 {ioapic / s / IoApicEnables [4%nat]: true} = d5 →
      restore_context_spec d5 = (rs´, d´) →
      serial_intr_handler_asm_spec rs d = Some (d´, rs´).
  Proof.
    intros d d1 d2 d3 d4 d5 d´ rs rs´ H H0 H1 H2 H3 H4 H5 H6 H7 H8.
    unfold serial_intr_handler_asm_spec.
    rewrite H, H0, H1, H2, H3, H4, H5, H6, H7, H8.
    reflexivity.
  Qed.


  Lemma serial_intr_handler_asm_eq_save_spec_restore:
    ∀ d d´ rs rs´,
      ikern d = true →
      ihost d = true →
      init d = true →
      in_intr d = true →
      serial_intr_handler_asm_spec rs d = Some (d´, rs´) →
      ∃ d1 d2 spec, save_context_spec rs d = d1 ∧
                    spec d1 = Some d2 ∧
                    restore_context_spec d2 = (rs´, d´).
  Proof.
    intros d d´ rs rs´ Hk Hh Hi Hr Ha.
    apply serial_intr_handler_asm_spec_inv in Ha. blast Ha.
    ∃ e. ∃ e3.
    esplit. repeat split.
    assumption.
  Qed.

  Lemma save_context_preserves_iflags:
    ∀ rs d d´,
      save_context_spec rs d = d´ →
      ( ikern d´ = ikern d ∧
        ihost d´ = ihost d ∧
        init d´ = init d ∧
        in_intr d´ = in_intr d
      ).
  Proof.
    intros rs d d´ H.
    functional inversion H; simpl.
    repeat (split; [reflexivity |]); reflexivity.
  Qed.

  Lemma serial_intr_handler_sw_spec_does_not_change_curr_intr_num:
    ∀ dx dy : RData,
      serial_intr_handler_sw_spec dx = Some dy →
      curr_intr_num dy = curr_intr_num dx.
  Proof.
    intros dx dy H.
    functional inversion H. subst.
    functional inversion H5. subst.
    functional inversion H6. subst.
    simpl. reflexivity.
    simpl. reflexivity.
  Qed.

  Lemma serial_intr_handler_sw_spec_does_not_change_tf:
    ∀ dx dy : RData,
      serial_intr_handler_sw_spec dx = Some dy →
      tf dy = tf dx.
  Proof.
    intros dx dy H.
    functional inversion H. subst.
    functional inversion H5. subst.
    functional inversion H6. subst.
    simpl. reflexivity.
    simpl. reflexivity.
  Qed.

  Lemma serial_intr_handler_sw_spec_independent_from_tf:
    ∀ (dx dy : RData) (x : TrapFrames),
      serial_intr_handler_sw_spec dx = Some dy →
      serial_intr_handler_sw_spec dx { tf : x} = Some dy { tf : x}.
  Proof.
    intros dx dy x.
    unfold serial_intr_handler_sw_spec.
    unfold lapic_eoi_spec.
    unfold cons_intr_aux.
    intros H. subdestruct; inversion H; reflexivity.
  Qed.

  Lemma serial_intr_handler_save_sw_restore_eq_asm:
    ∀ (rs rs´ : regset) (d d1 d2 d´ : RData),
      save_context_spec rs d = d1 →
      serial_intr_handler_sw_spec d1 = Some d2 →
      restore_context_spec d2 = (rs´, d´) →
      serial_intr_handler_asm_spec rs d = Some (d´, rs´).
  Proof.
    intros rs rs´ d d1 d2 d´ Hs Hsw Hr.
    unfold serial_intr_handler_asm_spec.
    functional inversion Hsw.
    generalize (save_context_preserves_iflags _ _ _ Hs).
    intros Hiflags. blast Hiflags. subst.
    rewrite H0, H1, H2, H3.
    change (Z.to_nat 4) with 4%nat in ×.
    rewrite H4. change (Pos.to_nat 4) with 4%nat in ×.
    rewrite H5. rewrite Hr. reflexivity.
  Qed.

  Section Serial_Intr_Handler_Refinement.

    Variable d: RData.

    Lemma serial_intr_handler_sw_to_asm:
    ∀ d´ rs,
      serial_intr_handler_sw_spec d = Some d´ →
      serial_intr_handler_asm_spec rs d = Some (d´, rs).
  Proof.
    intros d´ rs Hsw. generalize Hsw.
    apply save_restore_basic_rewrite; try auto.
    apply serial_intr_handler_save_sw_restore_eq_asm.
    apply serial_intr_handler_sw_spec_does_not_change_tf.
    apply serial_intr_handler_sw_spec_independent_from_tf.
  Qed.

  End Serial_Intr_Handler_Refinement.

End OBJ_X86Proof.