Library mcertikos.devdrivers.DHandlerCxtCode_serial_intr

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.

Require Import AbstractDataType.
Require Import HandlerOpGenSpec.
Require Import ObjInterruptController.
Require Import ObjConsole.
Require Import FutureTactic.
Require Import INVLemmaDriver.
Require Import ObjInterruptManagement.
Require Import CommonTactic.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import DHandlerCxt.
Require Import FutureTactic.
Require Import DHandlerCxtCSource.
Require Import ObjInterruptController.

Module DHANDLERCXTCODE.

  Section WithPrimitives.

    Context `{real_params: RealParams}.
    Context `{oracle_prop: MultiOracleProp}.
    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.

    Let mem := mwd (cdata RData).

    Context `{Hstencil: Stencil}.
    Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
    Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.

    Local Open Scope Z_scope.

    Section SERIAL_INTR_DISABLE_HANDLER.

      Let L: compatlayer (cdata RData) := serial_hw_intr ↦ gensem serial_hw_intr_spec
                                                         ⊕ serial_intr_handler_asm ↦ gensem serial_intr_handler_sw_spec
                                                         ⊕ iret ↦ gensem iret_spec
                                                         ⊕ serial_irq_check ↦ gensem serial_irq_check_spec.

      Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.

      Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

      Local Open Scope Z_scope.

      Section Serial_Intr_Disable_Body.

        Notation MAX := 100%Z.

        Lemma MAX_eq_INTR_DISABLE_REC_MAX:
          MAX = Z.of_nat INTR_DISABLE_REC_MAX. simpl. reflexivity. Qed.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

        Variables (ge: genv)
                  (STENCIL_MATCHES: stencil_matches sc ge).

        Variable (bserial_hw_intr: block).
        Hypothesis hserial_hw_intr1 : Genv.find_symbol ge serial_hw_intr = Some bserial_hw_intr.
        Hypothesis hserial_hw_intr2 : Genv.find_funct_ptr ge bserial_hw_intr =
                                      Some (External (EF_external serial_hw_intr
                                                                  (signature_of_type Tnil tuint
                                                                                     cc_default))
                                                     Tnil tuint cc_default).

        Variable (bserial_intr_handler_asm: block).
        Hypothesis hserial_intr_handler_asm1 : Genv.find_symbol ge serial_intr_handler_asm = Some bserial_intr_handler_asm.
        Hypothesis hserial_intr_handler_asm2 : Genv.find_funct_ptr ge bserial_intr_handler_asm =
                            Some (External (EF_external serial_intr_handler_asm
                                                        (signature_of_type Tnil tvoid
                                                                           cc_default))
                                           Tnil tvoid cc_default).

        Variable (biret: block).
        Hypothesis hiret1 : Genv.find_symbol ge iret = Some biret.
        Hypothesis hiret2 : Genv.find_funct_ptr ge biret =
                            Some (External (EF_external iret
                                                        (signature_of_type Tnil tvoid
                                                                           cc_default))
                                           Tnil tvoid cc_default).


        Variable (bserial_irq_check: block).
        Hypothesis hserial_irq_check1 : Genv.find_symbol ge serial_irq_check = Some bserial_irq_check.
        Hypothesis hserial_irq_check2 : Genv.find_funct_ptr ge bserial_irq_check =
                                        Some (External (EF_external serial_irq_check
                                                                    (signature_of_type Tnil tuint
                                                                                       cc_default))
                                                       Tnil tuint cc_default).

        Require Import ObjInterruptDriver.
        Lemma cons_intr_spec_subset:
          ∀ d d´ r,
            lapic_eoi_spec d = Some r →
            cons_intr_aux r = Some d´ →
            cons_intr_spec d = Some d´.
        Proof.
          intros.
          unfold cons_intr_spec. rewrite H, H0.
          functional inversion H. rewrite H4, H3, H5, H2.
          reflexivity.
        Qed.

        Lemma serial_hw_intr_range:
          ∀ d d´ n,
            init d = true →
            high_level_invariant d →
            serial_hw_intr_spec d = Some (d´, n) →
            n = 0 ∨ n = 36.
        Proof.
          assert (Hnat4: Z.to_nat 4 = 4%nat).
          {
            calc. reflexivity.
          }
          Opaque nth_error Z.to_nat.
          intros d d´ n Hinit Hinv H. functional inversion H.
          - subst. clear H H4. functional inversion H3; subst. clear H3.
            unfold s_ioapic´ in ×. clear s_ioapic´. unfold ioapic_trans_intr in H1.
            rewrite Hnat4 in H1.
            destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
            unfold update_CurrentIrq in H1; simpl in H1.
            inversion Hinv; simpl in ×.
            destruct (nth_error IoApicIrqs 4) eqn: Hirq.
            + generalize (valid_ioapic_state Hinit _ _ Hirq). intros [Hz [b Henable]].
              rewrite Henable in H1; simpl in H1. destruct b eqn: Hb; simpl in H1.
              × inversion H1. generalize Hz. toZ. replace (4 + 32) with 36 by omega. clear Hz. intros Hz. clear Hinv.
                subst.
                unfold s_lapic´ in ×. clear s_lapic´. unfold lapic_trans_intr in H4.
                destruct lapic; simpl in ×. destruct s; simpl in ×.
                rewrite Hz in *; simpl in ×. inversion H4.
                right. reflexivity.
              × inversion H1.
            + simpl in H1. inversion H1.
          - left. reflexivity.
          - left. reflexivity.
        Qed.
        Transparent nth_error Z.to_nat.

        Lemma serial_hw_intr_masked:
          ∀ d d´ n,
            serial_hw_intr_spec d = Some (d´, n) →
            n = 0 →
            d´ = d {com1: serial_intr (com1 d)}.
        Proof.
          intros.
          functional inversion H; subst. omega.
          unfold d´0 in ×. functional inversion H4; subst. reflexivity.
          unfold d´0 in ×. functional inversion H4; subst. reflexivity.
          reflexivity. reflexivity.
        Qed.

        Lemma serial_irq_check_range:
          ∀ d x,
            serial_irq_check_spec d = x →
            x = 0 ∨ x = 1.
        Proof.
          intros.
          unfold serial_irq_check_spec in H.
          destruct (SerialIrq (s (serial_intr (com1 d)))); subst.
          - right. reflexivity.
          - left . reflexivity.
        Qed.

        Lemma serial_irq_check_bound:
          ∀ d,
            0 ≤ serial_irq_check_spec d ≤ Int.max_unsigned.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold serial_irq_check_spec.
          destruct (SerialIrq (s (serial_intr (com1 d)))); subst.
          - omega.
          - omega.
        Qed.

        Lemma serial_intr_handler_true:
          ∀ d d´ b,
            SerialIrq (s (serial_intr (com1 d))) = true →
            serial_intr_handler d = Some (d´, b) →
            b = true.
        Proof.
          intros d d´ b H.
          unfold serial_intr_handler. unfold serial_hw_intr_spec. rewrite H. simpl.
          intros. subdestruct; inversion H0; reflexivity.
        Qed.

        Lemma serial_intr_handler_true_inv:
          ∀ d d´,
            serial_intr_handler d = Some (d´, true) →
            SerialIrq (s (serial_intr (com1 d))) = true.
        Proof.
          intros d d´.
          unfold serial_intr_handler. unfold serial_hw_intr_spec.
          intros. subdestruct; reflexivity.
        Qed.

        Lemma ioapic_trans_intr_preserves_length: ∀ d n,
                  Zlength (IoApicEnables (ioapic_trans_intr (IRQ n) (s (ioapic d))))
                  = Zlength (IoApicEnables (s (ioapic d))).
        Proof.
          intros.
          unfold ioapic_trans_intr.
          Opaque replace nth_error.
          destruct (s (ioapic d)); simpl.
          destruct (nth_error IoApicIrqs (Z.to_nat n)).
          destruct (nth_error IoApicEnables (Z.to_nat n)).
          destruct b;
          reflexivity.
          reflexivity.
          reflexivity.
        Qed.

        Lemma cons_intr_preserves_iflags:
          ∀ d d´,
            cons_intr_spec d = Some d´ →
            init d´ = init d ∧ ikern d´ = ikern d ∧ ihost d´ = ihost d.
        Proof.
          intros.
          functional inversion H; subst.
          functional inversion H0; functional inversion H5; simpl in *; subst; eauto.
        Qed.

        Lemma cons_intr_preserves_length:
          ∀ d d´,
            cons_intr_spec d = Some d´ →
            Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
        Proof.
          intros.
          functional inversion H; subst.
          functional inversion H0; functional inversion H5; simpl in *; subst; eauto.
        Qed.

        Lemma intr_flag_eq:
          ∀ d, intr_flag d = true → d = d {intr_flag: true}.
        Proof.
          intros.
          destruct d.
          simpl in ×.
          rewrite H.
          reflexivity.
        Qed.

        Lemma serial_intr_handler_refinement:
          ∀ d d´ b,
            ikern d = true →
            ihost d = true →
            init d = true →
            serial_intr_handler d = Some (d´, b) →
            serial_intr_handler_ext_spec d = Some (d´, b).
        Proof.
          intros d d´ b Hk Hh Hi.
          unfold serial_intr_handler_ext_spec.
          unfold serial_intr_handler.
          unfold serial_intr_handler_sw_spec.
          intros Hspec. rewrite Hk, Hh, Hi.
          subdestruct; eauto.
          subst.
          if_true. if_true. if_true. if_true.
          assumption.
          - functional inversion Hdestruct. simpl. functional inversion H2. simpl. auto.
          - functional inversion Hdestruct. simpl. functional inversion H2. simpl. auto.
          - functional inversion Hdestruct. simpl. functional inversion H2. simpl. auto.
          - functional inversion Hdestruct. simpl. functional inversion H2. simpl. auto.
        Qed.

        Lemma serial_intr_handler_ext_spec_inv:
          ∀ d d´ b,
            serial_intr_handler_ext_spec d = Some (d´, b) →
            ikern d = true ∧
            ihost d = true ∧
            init d = true ∧
            (
              (b = true ∧
               ∃ d0 d1,
                 serial_hw_intr_spec d = Some (d0, 36) ∧
                 serial_intr_handler_sw_spec d0 = Some d1 ∧
                 iret_spec d1 = Some d´
              )
              ∨
              (b = true ∧
               ∃ d0 n,
                 serial_hw_intr_spec d = Some (d0, n) ∧
                 n ≠ 36 ∧
                 d´ = d {com1: serial_intr (com1 d)}
              )
              ∨
              (b = false ∧
               serial_hw_intr_spec d = None
              )
            ).
        Proof.
          intros d d´ b. unfold serial_intr_handler_ext_spec. intros H.
          subdestruct; subst; inversion H.
          - repeat (split; [auto |]). left.
            split; [auto |].
            repeat esplit. assumption.
          - repeat (split; [auto |]). right. left.
            split; [auto |].
            repeat esplit. assumption.
          - repeat (split; [auto |]). right. right.
            split; [auto |].
            repeat esplit.
        Qed.

        Lemma serial_intr_handler_body_correct_irq:
          ∀ m d d´ env le t,
            ikern d = true →
            ihost d = true →
            init d = true →
            intr_flag d = true →
            0 < t ≤ Z.of_nat INTR_DISABLE_REC_MAX →
            env = PTree.empty _ →
            serial_intr_handler d = Some (d´, true) →
            high_level_invariant d →
            le ! _t = Some (Vint (Int.repr t)) →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) serial_intr_disable_handler_loop_body E0 le´ (m, d´) Out_normal ∧
              le´ ! _t = Some (Vint (Int.repr (t - 1))) ∧
              ((SerialIrq (s (serial_intr (com1 d´))) = true ∧
                le´ ! _has_irq = Some (Vint (Int.repr 1))) ∨
               (SerialIrq (s (serial_intr (com1 d´))) = false ∧
                le´ ! _has_irq = Some (Vint (Int.repr 0)))).
        Proof.
          generalize max_unsigned_val; intro muval. toZ.
          intros m d d´ env le t Hk Hh Hinit Hintr_flag Htrange Henv H Hinv Ht.
          exploit serial_intr_handler_refinement; try eassumption. intros Hspec.
          generalize (serial_intr_handler_ext_spec_inv _ _ _ Hspec).
          intros Hspecinv. blast Hspecinv. destruct Hspecinv4 as [Hc | [Hc | Hc]]; blast Hc; subst.
          -

            destruct (SerialIrq (s (serial_intr (com1 e0)))) eqn: Hirq´.
            + esplit.
              repeat vcgen.
              {
                unfold_RData.
                Opaque serial_intr.
                unfold serial_irq_check_spec; simpl. rewrite Hirq´. rewrite Int.unsigned_repr. reflexivity.
                omega.
              }
              {
                left. split.
                - unfold_RData. rewrite Hirq´. reflexivity.
                - ptreesolve.
              }
            + esplit.
              repeat vcgen.
              {
                unfold_RData.
                unfold serial_irq_check_spec; simpl. rewrite Hirq´. rewrite Int.unsigned_repr. reflexivity.
                omega.
              }
              {
                right. split.
                - unfold_RData. rewrite Hirq´. reflexivity.
                - ptreesolve.
              }
              
          -

            assert (Hn: e0 = 0 ∨ e0 = 36).
            {
              eapply serial_hw_intr_range; eassumption.
            }
            assert (Hed: e = d { com1 : serial_intr (com1 d)}).
            {
              assert (He0: e0 = 0) by omega.
              rewrite He0 in Hex1. functional inversion Hex1.
              - omega.
              - unfold d´. reflexivity.
              - functional inversion H3; unfold d´; rewrite H4; reflexivity.
            }
            destruct (SerialIrq (s (serial_intr (com1 (d { com1 : serial_intr (com1 d)}))))) eqn: Hirq´;
              unfold update_com1 in Hirq´; simpl in Hirq´.
            +
              esplit.
              repeat vcgen.
              {
                rewrite Int.unsigned_repr.
                rewrite Hed. unfold serial_irq_check_spec; simpl. rewrite Hirq´. reflexivity. omega.
              }
              {
                left. split.
                - reflexivity.
                - ptreesolve.
              }
            +
              esplit.
              repeat vcgen.
              {
                rewrite Int.unsigned_repr.
                rewrite Hed. unfold serial_irq_check_spec; simpl. rewrite Hirq´. reflexivity. omega.
              }
              {
                right. split.
                - reflexivity.
                - ptreesolve.
              }
          - esplit.
            repeat vcgen.
            Grab Existential Variables.
            apply le.
        Qed.

        Lemma serial_intr_handler_body_correct_noirq:
          ∀ d d´,
            serial_intr_handler d = Some (d´, false) →
            d´ = d.
        Proof.
          functional inversion 1. reflexivity.
        Qed.

        Function serial_intr_disable_concrete_rec (n: nat) (abd: RData) {struct n} : option (RData × bool) :=
          match n with
            | O ⇒ Some (abd, true)
            | S n´ ⇒
              match serial_intr_disable_concrete_rec n´ abd with
                | Some (d´, true) ⇒
                  match serial_intr_handler d´ with
                    | Some (d´´, true) ⇒ Some (d´´, true)
                    | Some (d´´, false) ⇒ Some (d´, false)
                    | None ⇒ None
                  end
                | Some (d´, false) ⇒ Some (d´, false)
                | None ⇒ None
              end
          end.

        Function serial_intr_disable_concrete_aux´ (n: nat) (abd: RData) {struct n} : option (RData × bool) :=
          match n with
            | O ⇒ Some (abd, true)
            | S n´ ⇒
              match serial_intr_handler abd with
                | Some (d´, true) ⇒ match serial_intr_disable_concrete_aux´ n´ d´ with
                                         | Some (d´´, true) ⇒ Some (d´´, true)
                                         | Some (d´´, false) ⇒ Some (d´´, false)
                                         | None ⇒ None
                                     end
                | Some (d´, false) ⇒ Some (abd, false)
                | None ⇒ None
              end
          end.

        Lemma aux_aux´_eq: ∀ n d d´,
              serial_intr_disable_concrete_aux n d = Some d´ →
              ∃ b,
                serial_intr_disable_concrete_aux´ n d = Some (d´, b).
        Proof.
          induction n.
          simpl.
          intros.
          inv H.
          esplit; reflexivity.
          simpl.
          intros.
          subdestruct.
          eapply IHn in H; eauto.
          destruct H.
          rewrite H.
          destruct x; esplit; reflexivity.
          inv H.
          esplit; reflexivity.
        Qed.

        Lemma tail_head_eq_true_rev: ∀ n d d1 d2 d3,
                              serial_intr_handler d = Some (d1, true) →
                              serial_intr_disable_concrete_rec n d = Some (d2, true) →
                              serial_intr_handler d2 = Some (d3, true) →
                              serial_intr_disable_concrete_rec n d1 = Some (d3, true).
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          rewrite H1 in H.
          inv H.
          reflexivity.
          simpl.
          intros.
          subdestruct.
          inv H0.
          eapply IHn in Hdestruct; eauto.
          rewrite Hdestruct.
          rewrite H1.
          reflexivity.
        Qed.

        Lemma rec_rev_true: ∀ n d d1 d2 d3,
                         serial_intr_handler d = Some (d1, true) →
                         serial_intr_disable_concrete_aux´ n d1 = Some (d2, true) →
                         serial_intr_disable_concrete_rec n d = Some (d3, true) →
                         ∃ d4,
                           serial_intr_handler d3 = Some (d4, true).
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          inv H1.
          esplit; eassumption.
          simpl.
          intros.
          subdestruct.
          inv H1.
          inv H0.
          generalize (tail_head_eq_true_rev _ _ _ _ _ H Hdestruct Hdestruct2); intro.
          eapply IHn in H0; eauto.
        Qed.

        Lemma rec_rev: ∀ n d d1 d2 d3 d4,
                         serial_intr_handler d = Some (d1, true) →
                         serial_intr_disable_concrete_aux´ n d1 = Some (d2, true) →
                         serial_intr_disable_concrete_rec n d = Some (d3, true) →
                         serial_intr_handler d3 = Some (d4, true) →
                         d2 = d4.
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          inv H1.
          rewrite H2 in H.
          inv H.
          reflexivity.
          simpl.
          intros.
          subdestruct.
          inv H1.
          inv H0.
          eapply IHn in Hdestruct8; eauto.
          generalize (tail_head_eq_true_rev _ _ _ _ _ H Hdestruct Hdestruct2); intro.
          assumption.
        Qed.

        Lemma tail_head_eq_true: ∀ n d d1 d2,
                              serial_intr_handler d = Some (d1, true) →
                              serial_intr_disable_concrete_rec n d1 = Some (d2, true) →
                              ∃ d3,
                                serial_intr_disable_concrete_rec n d = Some (d3, true) ∧
                                serial_intr_handler d3 = Some (d2, true).
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          esplit.
          split.
          reflexivity.
          assumption.
          simpl.
          intros.
          subdestruct.
          inv H0.
          eapply IHn in Hdestruct; eauto.
          destruct Hdestruct.
          destruct H0.
          rewrite H0, H1.
          esplit.
          split.
          reflexivity.
          assumption.
        Qed.

        Lemma tail_head_eq_false: ∀ n d d1 d2,
                              serial_intr_handler d = Some (d1, true) →
                              serial_intr_disable_concrete_rec n d1 = Some (d2, false) →
                              serial_intr_disable_concrete_rec (S n) d = Some (d2, false).
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          simpl.
          intros.
          subdestruct.
          inv H0.
          generalize (tail_head_eq_true _ _ _ _ H Hdestruct); intro.
          destruct H0.
          destruct H0.
          rewrite H0.
          rewrite H1.
          rewrite Hdestruct2.
          reflexivity.
          inv H0.
          eapply IHn in Hdestruct; eauto.
          simpl in ×.
          rewrite Hdestruct.
          reflexivity.
        Qed.

        Lemma aux´_rec_eq: ∀ n b d d´,
              serial_intr_disable_concrete_aux´ n d = Some (d´, b) →
              serial_intr_disable_concrete_rec n d = Some (d´, b).
        Proof.
          induction n.
          {
            simpl.
            intros.
            inv H.
            reflexivity.
          }
          {
            simpl.
            intros.
            subdestruct.
            {
              inv H.
              assert (∃ d´´, serial_intr_disable_concrete_aux´ n d = Some (d´´, true)).
              {
                clear IHn.
                revert Hdestruct.
                revert Hdestruct2.
                generalize dependent d.
                generalize dependent r.
                generalize dependent d´.
                induction n.
                simpl in ×.
                intros.
                esplit; reflexivity.
                simpl in ×.
                intros.
                rewrite Hdestruct in ×.
                subdestruct.
                inv Hdestruct2.
                generalize (IHn _ _ _ Hdestruct4 Hdestruct0); intro.
                destruct H.
                rewrite H.
                esplit; reflexivity.
              }
              destruct H.
              eapply IHn in H.
              rewrite H.
              generalize (rec_rev_true _ _ _ _ _ Hdestruct Hdestruct2 H); intro.
              destruct H0.
              rewrite H0.
              f_equal.
              f_equal.
              symmetry.
              eapply (rec_rev _ _ _ _ _ _ Hdestruct Hdestruct2 H H0); eauto.
            }
            {
              inv H.
              generalize Hdestruct2; intro Hrec.
              eapply IHn in Hrec.
              clear Hdestruct2.
              destruct n.
              simpl in ×.
              inv Hrec.
              simpl in ×.
              subdestruct.
              {
                inv Hrec.
                generalize (tail_head_eq_true _ _ _ _ Hdestruct Hdestruct0); intro.
                destruct H.
                destruct H.
                rewrite H.
                rewrite H0.
                rewrite Hdestruct3.
                reflexivity.
              }
              {
                inv Hrec.
                generalize (tail_head_eq_false _ _ _ _ Hdestruct Hdestruct0); intro.
                simpl in H.
                subdestruct.
                assumption.
                assumption.
              }
            }
            {
              inv H.
              functional inversion Hdestruct.
              subdestruct.
              inv H1.
              subst.
              generalize Hdestruct.
              clearAll.
              generalize dependent r.
              induction n.
              simpl.
              intros.
              rewrite Hdestruct.
              reflexivity.
              simpl.
              intros.
              rewrite IHn.
              reflexivity.
              assumption.
            }
          }
        Qed.


        Lemma serial_intr_disable_concrete_rec_has_irq:
          ∀ n d d´ dn b,
            serial_intr_disable_concrete_rec (S n) d = Some (d´, true) →
            serial_intr_disable_concrete_rec n d = Some (dn, b) →
            b = true.
        Proof.
          induction n.
          - simpl. inversion 2. reflexivity.
          - intros d d´ dn b Hsn Hn. remember (S n) as m.
            simpl in Hsn. rewrite Hn in Hsn. subdestruct. reflexivity.
        Qed.

        Lemma serial_intr_disable_concrete_rec_has_irq_exd:
          ∀ n d d´,
            serial_intr_disable_concrete_rec (S n) d = Some (d´, true) →
            ∃ dn, serial_intr_disable_concrete_rec n d = Some (dn, true).
        Proof.
          induction n.
          - simpl. inversion 1. ∃ d. reflexivity.
          - intros d d´ Hsn. remember (S n) as m.
            simpl in Hsn. subdestruct. ∃ r. reflexivity.
        Qed.

        Lemma serial_intr_disable_concrete_rec_has_irq_handler_true:
          ∀ n d d´ dn,
            serial_intr_disable_concrete_rec (S n) d = Some (d´, true) →
            serial_intr_disable_concrete_rec n d = Some (dn, true) →
            serial_intr_handler dn = Some (d´, true).
        Proof.
          intros n d d´ dn Hsn Hn.
          simpl in Hsn. rewrite Hn in Hsn.
          destruct (serial_intr_handler dn) eqn: Hhand. destruct p. destruct b.
          - rewrite Hsn. reflexivity.
          - inversion Hsn.
          - inversion Hsn.
        Qed.

        Lemma serial_intr_disable_concrete_rec_has_irq_handler_true_start:
          ∀ n d d´,
            (0 < n)%nat →
            serial_intr_disable_concrete_rec n d = Some (d´, true) →
            ∃ d1, serial_intr_handler d = Some (d1, true).
        Proof.
          induction n.
          - inversion 1.
          - intros d d´ Hlt Hsn. destruct n.
            + simpl in Hsn. subdestruct. ∃ r. reflexivity.
            + generalize Hsn. intros Hn.
              apply serial_intr_disable_concrete_rec_has_irq_exd in Hn.
              destruct Hn as [dn_1 Hn].
              apply IHn with (d´ := dn_1). omega. assumption.
        Qed.

        Lemma serial_intr_disable_concrete_rec_monotone:
          ∀ n i d d´,
            serial_intr_disable_concrete_rec n d = Some (d´, true) →
            (i ≤ n)%nat →
            ∃ dn,
              serial_intr_disable_concrete_rec i d = Some (dn, true).
        Proof.
          induction n.
          - simpl. intros. replace i with O in × by xomega. simpl in ×.
            esplit; reflexivity.
          - intros.
            assert ((i = S n ∨ i < S n)%nat) by xomega.
            Caseeq H1; intros.
            + subst. esplit; eauto.
            + exploit (serial_intr_disable_concrete_rec_has_irq_exd); eauto.
              intro. destruct H2. eapply IHn; eauto. omega.
        Qed.

        Lemma serial_intr_disable_concrete_rec_monotone_general:
          ∀ n i d d´ b1,
            serial_intr_disable_concrete_rec n d = Some (d´, b1) →
            (i ≤ n)%nat →
            ∃ dn b2,
              serial_intr_disable_concrete_rec i d = Some (dn, b2).
        Proof.
          induction n.
          simpl.
          intros.
          replace i with O in × by xomega.
          simpl in ×.
          esplit; esplit; reflexivity.
          intros.
          assert ((i = S n ∨ i < S n)%nat) by xomega.
          Caseeq H1; intros.
          subst.
          esplit; esplit; eauto.
          simpl in H.
          subdestruct.
          inv H.
          eapply IHn; eauto; xomega.
          inv H.
          eapply IHn; eauto; xomega.
          inv H.
          eapply IHn; eauto; xomega.
        Qed.

        Lemma serial_intr_disable_concrete_rec_all_has_irq_handler_true:
          ∀ i n d d´ dx,
            serial_intr_disable_concrete_rec n d = Some (d´, true) →
            (i < n)%nat →
            serial_intr_disable_concrete_rec i d = Some (dx, true) →
            ∃ dx´, serial_intr_handler dx = Some (dx´, true).
        Proof.
          intros.
          assert((S i ≤ n)%nat) by xomega.
          generalize (serial_intr_disable_concrete_rec_monotone n (S i) _ _ H H2); intro.
          destruct H3.
          simpl in H3.
          rewrite H1 in H3.
          subdestruct.
          inv H3.
          esplit; reflexivity.
        Qed.

        Lemma serial_intr_disable_concrete_rec_all_has_irq:
          ∀ i n d d´,
            serial_intr_disable_concrete_rec n d = Some (d´, true) →
            (i < n)%nat →
            ∃ dx, serial_intr_disable_concrete_rec i d = Some (dx, true).
        Proof.
          induction i.
          - simpl. intros. ∃ d. reflexivity.
          - intros n d d´ Hn Hlt. assert (Hlt´: (i < n)%nat) by omega.
            generalize (IHi n d d´ Hn Hlt´). intros [dx Hdx].
            simpl. rewrite Hdx.
            generalize (serial_intr_disable_concrete_rec_all_has_irq_handler_true i n d d´ dx Hn Hlt´ Hdx).
            intros [d´´ Hhand].
            ∃ d´´. rewrite Hhand. reflexivity.
        Qed.

        Lemma serial_intr_disable_concrete_rec_step_false:
          ∀ n d0 d d´,
            serial_intr_disable_concrete_rec n d0 = Some (d, true) →
            serial_intr_disable_concrete_rec (S n) d0 = Some (d´, false) →
            serial_intr_handler d = Some (d´, false).
        Proof.
          intros n d0 d d´ Hd Hd´.
          simpl in Hd´. rewrite Hd in Hd´.
          destruct (serial_intr_handler d) eqn: Hhand. destruct p. destruct b.
          - rewrite Hd´. reflexivity.
          - rewrite <- Hd´. functional inversion Hhand. reflexivity.
          - inversion Hd´.
        Qed.


        Lemma serial_intr_disable_concrete_rec_prev_step:
          ∀ n d d´,
            serial_intr_disable_concrete_rec (S n) d = Some (d´, false) →
            (serial_intr_disable_concrete_rec n d = Some (d´, false) ∨
             serial_intr_disable_concrete_rec n d = Some (d´, true)).
        Proof.
          induction n.
          - simpl. intros. subdestruct. inversion H. right. reflexivity.
          - intros. remember (S n) as sn. simpl in H.
            subdestruct.
            + subst. inversion H. right. reflexivity.
            + inversion H. left. reflexivity.
        Qed.

        Lemma serial_intr_disable_concrete_rec_false_middle:
          ∀ n d d´,
            serial_intr_disable_concrete_rec n d = Some (d´, false) →
            ∃ i, (i < n)%nat ∧
                 (∃ di, serial_intr_disable_concrete_rec i d = Some (di, true)) ∧
                 serial_intr_disable_concrete_rec (S i) d = Some (d´, false).
        Proof.
          induction n.
          - simpl.
            intros d d´ Hrec. inversion Hrec.
          - intros d d´ Hrec. exploit (serial_intr_disable_concrete_rec_prev_step). eapply Hrec.
            destruct 1 as [Ht | Hf].
            + apply IHn in Ht. destruct Ht as (i & Hirange & Hdi & Hdsi).
              ∃ i.
              split. omega.
              split. apply Hdi.
              apply Hdsi.
            + ∃ n.
              split. omega.
              split. ∃ d´. assumption.
              assumption.
        Qed.

        Lemma serial_intr_disable_concrete_rec_false_later:
          ∀ n i d d´,
            serial_intr_disable_concrete_rec i d = Some (d´, false) →
            (i < n)%nat →
            serial_intr_disable_concrete_rec n d = Some (d´, false).
        Proof.
          induction n.
          - simpl. intros i d d´ Hrec Hirange.
            replace i with O in × by omega. simpl in Hrec. inversion Hrec.
          - intros i d d´ Hrec Hirange.
            assert (Hicase: (i < n)%nat ∨ (i = n)%nat) by omega.
            destruct Hicase.
            + simpl. apply IHn in Hrec. rewrite Hrec. reflexivity. omega.
            + subst. simpl. rewrite Hrec. reflexivity.
        Qed.

        Lemma serial_intr_disable_concrete_rec_cases:
          ∀ n d d´ b,
            serial_intr_disable_concrete_rec n d = Some (d´, b) →
            ∃ i, (i ≤ n)%nat ∧
                 (∀ j, (j ≤ i)%nat →
                       (∃ dj, serial_intr_disable_concrete_rec j d = Some (dj, true))) ∧
                 (∀ j, (i < j ≤ n)%nat →
                       (serial_intr_disable_concrete_rec j d = Some (d´, false))).
        Proof.
          intros n d d´ b Hrec.
          destruct b.
          - ∃ n. split. omega.
            split. intros.
            exploit (serial_intr_disable_concrete_rec_monotone); eauto.
            intros. omega.
          - exploit (serial_intr_disable_concrete_rec_false_middle). eassumption.
            intros Hcase. destruct Hcase as (i & Hirange & (di & Hdi) & Hdsi).
            ∃ i. split. omega.
            split. intros. exploit (serial_intr_disable_concrete_rec_monotone); eauto.
            intros. assert (Hjcase: j = S i ∨ (j > (S i))%nat) by omega.
            destruct Hjcase.
            + subst. assumption.
            + exploit (serial_intr_disable_concrete_rec_false_later j (S i) d d´). assumption. omega.
              auto.
        Qed.

        Lemma serial_intr_disable_concrete_loop_body_rec_correct:
          ∀ m d0 d d´ env le t,
            ikern d = true →
            ihost d = true →
            init d = true →
            intr_flag d = true →
            0 < t ≤ MAX →
            env = PTree.empty _ →
            serial_intr_disable_concrete_rec (Z.to_nat (MAX - t)) d0 = Some (d, true) →
            serial_intr_disable_concrete_rec (S (Z.to_nat (MAX - t))) d0 = Some (d´, true) →
            high_level_invariant d →
            le ! _t = Some (Vint (Int.repr t)) →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) serial_intr_disable_handler_loop_body E0 le´ (m, d´) Out_normal ∧
              le´ ! _t = Some (Vint (Int.repr (t - 1))) ∧
              ((SerialIrq (s (serial_intr (com1 d´))) = true ∧
                le´ ! _has_irq = Some (Vint (Int.repr 1))) ∨
               (SerialIrq (s (serial_intr (com1 d´))) = false ∧
                le´ ! _has_irq = Some (Vint (Int.repr 0)))).
        Proof.
          intros m d0 d d´ env le t Hk Hh Hinit Hintr_flag Htrange Henv Hd Hd´ Hinv Hlet.
          generalize Hd´. intros rHd´. remember (Z.to_nat (100 - t)) as n. simpl in Hd´.
          rewrite Hd in Hd´.
          destruct (serial_intr_handler d) eqn: Heqerror. destruct p.
          - destruct b eqn: Hb.
            + inversion Hd´.
              simpl in rHd´.
              exploit (serial_intr_handler_body_correct_irq m d d´ env le t Hk Hh Hinit Hintr_flag Htrange Henv); try assumption.
              subst. assumption.
              intros Hexec.
              apply Hexec.
            + inversion Hd´.
          - inversion Hd´.
        Qed.

        Lemma serial_intr_handler_not_none:
          ∀ n d0 d´,
            serial_intr_disable_concrete_aux (S n) d0 = Some d´ →
            serial_intr_handler d0 ≠ None.
        Proof.
          simpl. intros. subdestruct.
        Qed.

        Lemma serial_intr_disable_concrete_rec_preserves_ikern:
          ∀ n d d´,
            ikern d = true →
            serial_intr_disable_concrete_rec n d = Some (d´, true) →
            ikern d´ = true.
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          assumption.
          simpl.
          intros.
          subdestruct.
          inv H0.
          functional inversion Hdestruct2; subst.
          functional inversion H5; functional inversion H4; functional inversion H3; subst; eauto.
          simpl.
          eapply IHn; eauto.
        Qed.

        Lemma serial_intr_disable_concrete_rec_preserves_ihost:
          ∀ n d d´,
            ihost d = true →
            serial_intr_disable_concrete_rec n d = Some (d´, true) →
            ihost d´ = true.
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          assumption.
          simpl.
          intros.
          subdestruct.
          inv H0.
          functional inversion Hdestruct2; subst.
          functional inversion H5; functional inversion H4; functional inversion H3; subst; eauto.
          simpl.
          eapply IHn; eauto.
        Qed.

        Lemma serial_intr_disable_concrete_rec_preserves_init:
          ∀ n d d´,
            init d = true →
            serial_intr_disable_concrete_rec n d = Some (d´, true) →
            init d´ = true.
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          assumption.
          simpl.
          intros.
          subdestruct.
          inv H0.
          functional inversion Hdestruct2; subst.
          functional inversion H5; functional inversion H4; functional inversion H3; subst; eauto.
          simpl.
          eapply IHn; eauto.
        Qed.

        Lemma serial_intr_disable_concrete_rec_preserves_intr_flag:
          ∀ n d d´ b,
            intr_flag d = true →
            serial_intr_disable_concrete_rec n d = Some (d´, b) →
            intr_flag d´ = true.
        Proof.
          induction n.
          simpl.
          intros.
          inv H0.
          assumption.
          simpl.
          intros.
          subdestruct.
          inv H0.
          functional inversion Hdestruct2; subst.
          functional inversion H5; functional inversion H4; functional inversion H3; subst; eauto.
          simpl.
          eapply IHn; eauto.
          inv H0.
          eapply IHn; eauto.
          inv H0.
          eapply IHn; eauto.
        Qed.

        Lemma serial_intr_disable_concrete_rec_preserves_high_level_invariant:
          ∀ i d di,
            high_level_invariant d →
            serial_intr_disable_concrete_rec i d = Some (di, true) →
            high_level_invariant di.
        Proof.
          induction i.
          simpl.
          intros.
          inv H0.
          assumption.
          simpl.
          intros.
          subdestruct.
          inv H0.
          eapply IHi in Hdestruct; eauto.
          inv Hdestruct.

          functional inversion Hdestruct2; subst.
          functional inversion H5; functional inversion H4; functional inversion H3; functional inversion H1; functional inversion H24; simpl in *; subst; constructor; unfold s_ioapic´ in *; simpl in *; eauto.
          unfold ioapic_trans_intr.
          destruct (s (ioapic r)).
          destruct (nth_error IoApicIrqs (Z.to_nat 4)).
          destruct (nth_error IoApicEnables (Z.to_nat 4)).
          destruct b.
          apply valid_ioapic_max_intr.
          apply valid_ioapic_max_intr.
          apply valid_ioapic_max_intr.
          apply valid_ioapic_max_intr.

          rewrite replace_replace.
          rewrite replace_preserves_Zlength.
          unfold ioapic_trans_intr.
          destruct (s (ioapic r)).
          destruct (nth_error IoApicIrqs (Z.to_nat 4)).
          destruct (nth_error IoApicEnables (Z.to_nat 4)).
          destruct b.
          simpl; assumption.
          simpl; assumption.
          simpl; assumption.
          simpl; assumption.

          unfold ioapic_trans_intr.
          destruct (s (ioapic r)).
          destruct (nth_error IoApicIrqs (Z.to_nat 4)).
          destruct (nth_error IoApicEnables (Z.to_nat 4)).
          destruct b.
          intros;
          simpl in ×.
          rewrite replace_replace.
          generalize (valid_ioapic_state H0 _ _ H6); intro tmp.
          destruct tmp.
          destruct H21.
          assert (ncase: n = 4%nat ∨ n ≠ 4%nat) by omega.
          case_eq ncase; intros.
          subst.
          rewrite nth_error_replace_gss.
          split.
          reflexivity.
          esplit; reflexivity.
          generalize (nth_error_range _ _ _ _ H21); intro.
          xomega.
          rewrite nth_error_replace_gso.
          eapply valid_ioapic_state; eauto.
          change (Pos.to_nat 4%positive) with 4%nat.
          omega.

          intros;
          simpl in ×.
          rewrite replace_replace.
          generalize (valid_ioapic_state H0 _ _ H6); intro tmp.
          destruct tmp.
          destruct H21.
          assert (ncase: n = 4%nat ∨ n ≠ 4%nat) by omega.
          case_eq ncase; intros.
          subst.
          rewrite nth_error_replace_gss.
          split.
          reflexivity.
          esplit; reflexivity.
          generalize (nth_error_range _ _ _ _ H21); intro.
          xomega.
          rewrite nth_error_replace_gso.
          eapply valid_ioapic_state; eauto.
          change (Pos.to_nat 4%positive) with 4%nat.
          omega.

          intros;
          simpl in ×.
          rewrite replace_replace.
          generalize (valid_ioapic_state H0 _ _ H6); intro tmp.
          destruct tmp.
          destruct H21.
          assert (ncase: n = 4%nat ∨ n ≠ 4%nat) by omega.
          case_eq ncase; intros.
          subst.
          rewrite nth_error_replace_gss.
          split.
          reflexivity.
          esplit; reflexivity.
          generalize (nth_error_range _ _ _ _ H21); intro.
          xomega.
          rewrite nth_error_replace_gso.
          eapply valid_ioapic_state; eauto.
          change (Pos.to_nat 4%positive) with 4%nat.
          omega.

          intros;
          simpl in ×.
          rewrite replace_replace.
          generalize (valid_ioapic_state H0 _ _ H6); intro tmp.
          destruct tmp.
          destruct H21.
          assert (ncase: n = 4%nat ∨ n ≠ 4%nat) by omega.
          case_eq ncase; intros.
          subst.
          rewrite nth_error_replace_gss.
          split.
          reflexivity.
          esplit; reflexivity.
          generalize (nth_error_range _ _ _ _ H21); intro.
          xomega.
          rewrite nth_error_replace_gso.
          eapply valid_ioapic_state; eauto.
          change (Pos.to_nat 4%positive) with 4%nat.
          omega.
          omega.

          unfold ioapic_trans_intr.
          destruct (s (ioapic r)).
          destruct (nth_error IoApicIrqs (Z.to_nat 4)).
          destruct (nth_error IoApicEnables (Z.to_nat 4)).
          destruct b.
          apply valid_ioapic_max_intr.
          apply valid_ioapic_max_intr.
          apply valid_ioapic_max_intr.
          apply valid_ioapic_max_intr.

          unfold ioapic_trans_intr.
          destruct (s (ioapic r)).
          destruct (nth_error IoApicIrqs (Z.to_nat 4)).
          destruct (nth_error IoApicEnables (Z.to_nat 4)).
          destruct b.
          rewrite replace_replace.
          rewrite replace_preserves_Zlength.
          unfold ioapic_trans_intr.
          destruct (s (ioapic r)).
          destruct (nth_error IoApicIrqs (Z.to_nat 4)).
          destruct (nth_error IoApicEnables (Z.to_nat 4)).
          destruct b.
          apply valid_ioapic_enables.
          apply valid_ioapic_enables.
          apply valid_ioapic_enables.
          apply valid_ioapic_enables.

          rewrite replace_replace.
          rewrite replace_preserves_Zlength.
          simpl; assumption.

          rewrite replace_replace.
          rewrite replace_preserves_Zlength.
          simpl; assumption.

          rewrite replace_replace.
          rewrite replace_preserves_Zlength.
          unfold ioapic_trans_intr.
          destruct (s (ioapic r)).
          destruct (nth_error IoApicIrqs (Z.to_nat 4)).
          destruct (nth_error IoApicEnables (Z.to_nat 4)).
          destruct b.
          simpl; assumption.
          simpl; assumption.
          simpl; assumption.
          simpl; assumption.

          unfold ioapic_trans_intr.
          destruct (s (ioapic r)).
          destruct (nth_error IoApicIrqs (Z.to_nat 4)).
          destruct (nth_error IoApicEnables (Z.to_nat 4)).
          destruct b.
          intros;
          simpl in ×.
          rewrite replace_replace.
          generalize (valid_ioapic_state H0 _ _ H6); intro tmp.
          destruct tmp.
          destruct H21.
          assert (ncase: n = 4%nat ∨ n ≠ 4%nat) by omega.
          case_eq ncase; intros.
          subst.
          rewrite nth_error_replace_gss.
          split.
          reflexivity.
          esplit; reflexivity.
          generalize (nth_error_range _ _ _ _ H21); intro.
          xomega.
          rewrite nth_error_replace_gso.
          eapply valid_ioapic_state; eauto.
          change (Pos.to_nat 4%positive) with 4%nat.
          omega.

          intros;
          simpl in ×.
          rewrite replace_replace.
          generalize (valid_ioapic_state H0 _ _ H6); intro tmp.
          destruct tmp.
          destruct H21.
          assert (ncase: n = 4%nat ∨ n ≠ 4%nat) by omega.
          case_eq ncase; intros.
          subst.
          rewrite nth_error_replace_gss.
          split.
          reflexivity.
          esplit; reflexivity.
          generalize (nth_error_range _ _ _ _ H21); intro.
          xomega.
          rewrite nth_error_replace_gso.
          eapply valid_ioapic_state; eauto.
          change (Pos.to_nat 4%positive) with 4%nat.
          omega.

          intros;
          simpl in ×.
          rewrite replace_replace.
          generalize (valid_ioapic_state H0 _ _ H6); intro tmp.
          destruct tmp.
          destruct H21.
          assert (ncase: n = 4%nat ∨ n ≠ 4%nat) by omega.
          case_eq ncase; intros.
          subst.
          rewrite nth_error_replace_gss.
          split.
          reflexivity.
          esplit; reflexivity.
          generalize (nth_error_range _ _ _ _ H21); intro.
          xomega.
          rewrite nth_error_replace_gso.
          eapply valid_ioapic_state; eauto.
          change (Pos.to_nat 4%positive) with 4%nat.
          omega.

          intros;
          simpl in ×.
          rewrite replace_replace.
          generalize (valid_ioapic_state H0 _ _ H6); intro tmp.
          destruct tmp.
          destruct H21.
          assert (ncase: n = 4%nat ∨ n ≠ 4%nat) by omega.
          case_eq ncase; intros.
          subst.
          rewrite nth_error_replace_gss.
          split.
          reflexivity.
          esplit; reflexivity.
          generalize (nth_error_range _ _ _ _ H21); intro.
          xomega.
          rewrite nth_error_replace_gso.
          eapply valid_ioapic_state; eauto.
          change (Pos.to_nat 4%positive) with 4%nat.
          omega.
          omega.
          econstructor; simpl in *; eauto.
        Qed.

        Lemma in_intr_update:
          ∀ d b,
            in_intr d = b →
            d = d { in_intr: b }.
        Proof.
          intros.
          unfold update_in_intr; simpl. rewrite <- H.
          destruct d. reflexivity.
        Qed.

        Section FunctionalDischarge.
          Variables A B C D: Type.

          Variable f1: A → (B × C).
          Variable f2: A → D → (B × C).

          Variable a: A.
          Variable b: B.
          Variable c: C.
          Variable d: D.

          Lemma func1_return_pair:
            f1 a = (fst (f1 a), snd (f1 a)).
          Proof.
            destruct (f1 a) eqn: Hfa.
            simpl. reflexivity.
          Qed.

          Lemma func2_return_pair:
            f2 a d = (fst (f2 a d), snd (f2 a d)).
          Proof.
            destruct (f2 a d) eqn: Hfa.
            simpl. reflexivity.
          Qed.
        End FunctionalDischarge.

        Transparent serial_intr.
        Lemma serial_intr_disable_concrete_rec_irq_true:
          ∀ i d di dsi b,
            serial_intr_disable_concrete_rec i d = Some (di, true) →
            SerialIrq (s (serial_intr (com1 di))) = true →
            serial_intr_disable_concrete_rec (S i) d = Some (dsi, b) →
            b = true.
        Proof.
          simpl.
          intros.
          subdestruct.
          inv H1.
          reflexivity.
          functional inversion Hdestruct2.
          subdestruct.
          inv H4.
          subst.
          functional inversion H3; subst.
          unfold d´ in ×.
          inv H.
          inv H1.
          unfold serial_intr in H2.
          simpl in H2.
          rewrite H0 in H2.
          inv H2.
        Qed.

        Lemma serial_intr_disable_concrete_rec_false:
          ∀ n d di,
            serial_intr_disable_concrete_rec n d = Some (di, true) →
            SerialIrq (s (serial_intr (com1 di))) = false →
            (n < 100)%nat →
            serial_intr_disable_concrete_rec INTR_DISABLE_REC_MAX d = Some (di, false).
        Proof.
          remember (100%nat) as m.
          clear Heqm.
          induction m.
          simpl.
          intros.
          xomega.
          intros.
          assert ((n = m ∨ n < m)%nat) by xomega.
          Caseeq H2; intros.
          subst.
          simpl in ×.
          rewrite H.
          unfold serial_intr_handler, serial_hw_intr_spec.
          unfold serial_intr; simpl.
          rewrite H0.
          reflexivity.
          eapply IHm in H; eauto.
          simpl.
          destruct (serial_intr_disable_concrete_rec m d).
          destruct p.
          unfold serial_intr_handler, serial_hw_intr_spec.
          inv H.
          reflexivity.
          inv H.
        Qed.

        Section serial_intr_disable_concrete_loop_proof.
          Variable m_init: memb.
          Variable d: RData.
          Variable d_end: RData.
          Variable b_end: bool.
          Variable K: nat.

          Hypothesis Hinv: high_level_invariant d.
          Hypothesis Hkern: ikern d = true.
          Hypothesis Hhost: ihost d = true.
          Hypothesis Hinit: init d = true.
          Hypothesis Hintr_flag: intr_flag d = true.
          Hypothesis Hirq: SerialIrq (s (serial_intr (com1 d))) = true.
          Hypothesis HKrange: (0 < K ≤ INTR_DISABLE_REC_MAX)%nat.
          Hypothesis Hcorrect: serial_intr_disable_concrete_rec INTR_DISABLE_REC_MAX d = Some (d_end, b_end).
          Hypothesis HK1: ∀ j, (j ≤ K)%nat →
                       (∃ dj, serial_intr_disable_concrete_rec j d = Some (dj, true)).
          Hypothesis HK2: ∀ j, (K < j ≤ INTR_DISABLE_REC_MAX)%nat →
                       (serial_intr_disable_concrete_rec j d = Some (d_end, false)).

          Function serial_intr_disable_concrete_loop_body_P (le: temp_env) (m: mem): Prop :=
            le ! _has_irq = Some (Vint (Int.repr 1)) ∧
            le ! _t = Some (Vint (Int.repr (Z.of_nat INTR_DISABLE_REC_MAX))) ∧
            m = (m_init, d).


          Function serial_intr_disable_concrete_loop_body_Q (le : temp_env) (m: mem): Prop :=
            ∃ d_end b,
            serial_intr_disable_concrete_rec INTR_DISABLE_REC_MAX d = Some (d_end, b) ∧
            (le ! _has_irq = Some (Vint (Int.repr 0)) ∨
             le ! _t = Some (Vint (Int.repr 0))) ∧
            m = (m_init, d_end).

          Lemma serial_intr_disable_concrete_loop_correct_aux:
            LoopProofSimpleWhile.t
              serial_intr_disable_handler_loop_condition
              serial_intr_disable_handler_loop_body
              ge (PTree.empty _)
              serial_intr_disable_concrete_loop_body_P
              serial_intr_disable_concrete_loop_body_Q.
          Proof.
            generalize max_unsigned_val; intro muval.
            apply LoopProofSimpleWhile.make with
            (W := Z)
              (lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
              (I := fun le m w ⇒ ∃ i di,
                                    le ! _t = Some (Vint (Int.repr w)) ∧
                                    w = 100 - i ∧
                                    intr_flag di = true ∧
                                    ((
                                        0 ≤ i < Z.of_nat K ∧
                                        m = (m_init, di) ∧
                                        serial_intr_disable_concrete_rec (Z.to_nat i) d = Some (di, true) ∧
                                        SerialIrq (s (serial_intr (com1 di))) = true ∧
                                        le ! _has_irq = Some (Vint (Int.repr 1))
                                      ) ∨ (
                                       i = Z.of_nat K ∧
                                       m = (m_init, di) ∧
                                        serial_intr_disable_concrete_rec (Z.to_nat i) d = Some (di, true) ∧
                                        (
                                          (K = 100%nat ∧
                                            SerialIrq (s (serial_intr (com1 di))) = true ∧
                                            le ! _has_irq = Some (Vint (Int.repr 1))) ∨
                                          (
                                            SerialIrq (s (serial_intr (com1 di))) = false ∧
                                           le ! _has_irq = Some (Vint (Int.repr 0)))
                                        )
                                     ))).
            apply Zwf_well_founded.
            intros le m Hp.
            destruct Hp as (Hp1 & Hp2 & Hp3).
            ∃ 100, 0, d.
            rewrite Hp3. simpl.
            split. assumption.
            split. reflexivity.
            split. assumption.
            left. split; auto. omega.

            intros le m w Hi.
            destruct Hi as (i & di & Hlet & Hwt & Hdi_intr_flag & Hcond).
            destruct Hcond as [Hmid | Hnoirq].
            Case "in loop".
            {
              destruct Hmid as (Hirange & Hm & Hrec & HhasIrq & Hle).
              rewrite Hm in ×.
              {