Library mcertikos.devdrivers.DLApicCode_cons_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 FutureTactic.
Require Import List.

Require Import AbstractDataType.
Require Import DLApicCSource.
Require Import ConsoleGenSpec.
Require Import ObjSerialDriver.
Require Import ObjConsole.
Require Import DLApic.
Require Import INVLemmaDevice.
Require Import DeviceStateDataType.

Require Import TacticsForTesting.
Require Import OracleInstances.

Module DLAPICCODE.

  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 CONSINTR.

      Let L: compatlayer (cdata RData) :=
        serial_getc ↦ gensem serial_getc_spec
      ⊕ lapic_eoi ↦ gensem lapic_eoi_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 ConsIntrBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable (bserial_getc: block).
        Hypothesis hserial_getc1 : Genv.find_symbol ge serial_getc = Some bserial_getc.
        Hypothesis hserial_getc2 : Genv.find_funct_ptr ge bserial_getc =
                                   Some (External (EF_external serial_getc
                                                               (signature_of_type Tnil tuint cc_default))
                                                  Tnil tuint cc_default).

        Variable (blapic_eoi: block).
        Hypothesis hlapic_eoi1 : Genv.find_symbol ge lapic_eoi = Some blapic_eoi.
        Hypothesis hlapic_eoi2 : Genv.find_funct_ptr ge blapic_eoi =
                                   Some (External (EF_external lapic_eoi
                                                               (signature_of_type Tnil tvoid cc_default))
                                                  Tnil tvoid cc_default).

        Notation CONS_BUFFER_MAX_CHARS := (CONS_BUFFER_SIZE - 1).

        Ltac unfold_all :=
          unfold_SerialState; unfold update_cons_buf, update_rpos; simpl; unfold_DeviceData;
          unfold update_com1; simpl; unfold update_console; simpl.

        Section cons_intr_loop_proof.

          Variable m_init: memb.
          Variable abd: RData.

          Variable str: list Z.
          Variable h: Z.
          Variable t: list Z.

          Variable c: Z.

          Variable cd: ConsoleDriver.

          Hypothesis Hrx: (RxBuf (s (com1 abd))) = t.
          Hypothesis HtxBuf: (TxBuf (s (com1 abd))) = nil.
          Hypothesis Hon: (SerialOn (s (com1 abd))) = true.
          Hypothesis HrxIntMask: (RxIntEnable (s (com1 abd))) = true.
          Hypothesis HserIntr: (SerialIrq (s (com1 abd))) = false.
          Hypothesis Hdlab: (DLAB (s (com1 abd))) = false.
          Hypothesis Hinv: high_level_invariant abd.
          Hypothesis Hkern: ikern abd = true.
          Hypothesis Hinit: init abd = true.
          Hypothesis Hhost: ihost abd = true.
          Hypothesis Hserex: serial_exists (drv_serial abd) = 1.
          Hypothesis Hrpos: 0 ≤ rpos cd < 512.
          Hypothesis Hos: str = h :: t.
          Hypothesis Hc: last str 0 = c.
          Hypothesis Hslen: Zlength str ≤ 12.
          Hypothesis Hschar: Forall isChar str.
          Hypothesis Hevents: ∀ n, n ≤ (Zlength str) × 2 + 2
                                   → SerialEnv ((l1 (com1 abd)) + n) = NullEvent.

          Notation CONS_BUFFER_MAX_CHARS := (CONS_BUFFER_SIZE - 1).
          Notation CONS_BUFFER_MAX_DW := (CONS_BUFFER_SIZE - 2).
          Notation CBL_MAX_CHARS := (CONS_BUFFER_SIZE - 2).
          Notation CBL_MAX_DW := (CONS_BUFFER_SIZE - 3).

          Definition cons_buf_mid (i: Z) :=
            if (zle_le 0 i (Zlength str - 1))
            then
              if (zle (i + 1 + Zlength (cons_buf cd)) CONS_BUFFER_MAX_CHARS)
              then ((cons_buf (cd)) ++ firstn (Z.to_nat i + 1)%nat str)
              else skipn (Z.to_nat (i + 1 + Zlength (cons_buf (cd)) - CONS_BUFFER_MAX_CHARS))
                         ((cons_buf (cd)) ++ firstn (Z.to_nat i + 1)%nat str)
            else
              if (zle (Zlength str + Zlength (cons_buf cd)) CONS_BUFFER_MAX_DW)
              then (cons_buf (cd) ++ str)
              else skipn (Z.to_nat (Zlength str + Zlength (cons_buf (cd)) - CONS_BUFFER_MAX_CHARS))
                         ((cons_buf (cd)) ++ str).

          Definition rpos_mid (i: Z) :=
            if zle (Zlength (cons_buf (cd)) + i + 1) CONS_BUFFER_MAX_CHARS
            then (rpos cd)
            else if (zle_le 0 i (Zlength str - 1))
                 then
                   (rpos cd + Zlength (cons_buf (cd)) + i + 2) mod CONS_BUFFER_SIZE
                 else
                   (rpos cd + Zlength (cons_buf (cd)) + Zlength str + 1) mod CONS_BUFFER_SIZE.

          Hypothesis Hcons: console abd = mkConsoleDrvier (cons_buf_mid 0) (rpos_mid 0).

          Definition cons_intr_loop_body_P (le: temp_env) (m: mem): Prop :=
            le ! _hasMore = Some (Vint (Int.one)) ∧
            le ! _t = Some (Vint (Int.zero)) ∧
            m = (m_init, abd).

          Definition d_end :=
            (abd {com1 / l1: (l1 (com1 abd)) + (Zlength t) × 2 + 1}
                 {com1 / s / RxBuf: nil}
                 {com1 / s / SerialIrq: false}
                 {console / cons_buf: cons_buf_mid (Zlength str)}
                 {console / rpos: rpos_mid (Zlength str)}).

          Definition cons_intr_loop_body_Q (le : temp_env) (m: mem): Prop :=
            m = (m_init, d_end).

          Lemma cIsChar:
            isChar c.
          Proof.
            subst c. apply forall_last. assumption. unfold isChar. omega.
          Qed.

          Lemma cons_buf_mid_le_max_dw:
            ∀ i,
              0 ≤ i →
              Zlength (cons_buf_mid i) ≤ CONS_BUFFER_MAX_CHARS.
          Proof.
            intros. unfold cons_buf_mid.
            case_if.
            - case_if.
              + repeat solve_list. rewrite min_l. repeat toZ; omega. repeat toZ; omega.
              + repeat solve_list. rewrite min_l. repeat toZ; omega. repeat toZ; omega.
            - destruct o; [omega |].
              case_if.
              + repeat solve_list. omega.
              + repeat solve_list. repeat toZ; omega.
          Qed.

          Lemma cons_buf_mid_lt_max_dw:
            ∀ i,
              0 ≤ i ≤ Zlength str - 1 →
              i + 1 + Zlength (cons_buf cd) < CONS_BUFFER_MAX_CHARS →
              Zlength (cons_buf_mid i) < CONS_BUFFER_MAX_CHARS.
          Proof.
            unfold cons_buf_mid.
            remember (Zlength str) as ls.
            remember (Zlength (cons_buf cd)) as lb.
            intros. rewrite zle_le_true by omega.
            rewrite zle_true by omega.
            repeat solve_list. rewrite min_l. repeat toZ; try omega.
            repeat toZ; try omega.
          Qed.

          Lemma cons_buf_mid_eq_max_dw0:
            ∀ i,
              0 ≤ i ≤ Zlength str - 1 →
              i + 1 + Zlength (cons_buf cd) = CONS_BUFFER_MAX_CHARS →
              Zlength (cons_buf_mid i) = CONS_BUFFER_MAX_CHARS.
          Proof.
            unfold cons_buf_mid.
            remember (Zlength str) as ls.
            remember (Zlength (cons_buf cd)) as lb.
            intros. rewrite zle_le_true by omega.
            rewrite zle_true by omega.
            repeat solve_list. rewrite min_l. repeat toZ; try omega.
            repeat toZ; try omega.
          Qed.

          Lemma cons_buf_mid_eq_max_dwn:
            ∀ i,
              0 ≤ i ≤ Zlength str - 1 →
              i + 1 + Zlength (cons_buf cd) > CONS_BUFFER_MAX_CHARS →
              Zlength (cons_buf_mid i) = CONS_BUFFER_MAX_CHARS.
          Proof.
            unfold cons_buf_mid.
            remember (Zlength str) as ls.
            remember (Zlength (cons_buf cd)) as lb.
            intros. rewrite zle_le_true by omega.
            rewrite zle_false by omega.
            repeat solve_list. rewrite min_l. repeat toZ; try omega.
            repeat toZ; try omega.
          Qed.

          Lemma cons_buf_mid_eq_max_dw:
            ∀ i,
              0 ≤ i ≤ Zlength str - 1 →
              i + 1 + Zlength (cons_buf cd) ≥ CONS_BUFFER_MAX_CHARS →
              Zlength (cons_buf_mid i) = CONS_BUFFER_MAX_CHARS.
          Proof.
            intros.
            assert (Hcase: i + 1 + Zlength (cons_buf cd) > CONS_BUFFER_MAX_CHARS
                           ∨ i + 1 + Zlength (cons_buf cd) = CONS_BUFFER_MAX_CHARS) by omega.
            Caseeq Hcase.
            apply cons_buf_mid_eq_max_dwn. assumption.
            apply cons_buf_mid_eq_max_dw0. assumption.
          Qed.

          Lemma rpos_mid_succ_still:
            ∀ {i},
              0 ≤ i →
              i + 1 + Zlength (cons_buf cd) < CONS_BUFFER_MAX_DW →
              rpos_mid i = rpos_mid (i + 1).
          Proof.
            intros. unfold rpos_mid. repeat rewrite zle_true; try omega.
          Qed.

          Lemma cons_buf_mid_succ_still:
            ∀ z stl x tlstl i,
              0 ≤ i →
              str = z :: stl →
              skipn (Z.to_nat i) stl = x :: tlstl →
              i + 1 + Zlength (cons_buf cd) ≤ CBL_MAX_DW →
              cons_buf_mid (i + 1) = cons_buf_mid i ++ x :: nil.
          Proof.
            intros.
            assert (Hi: 0 ≤ i < Zlength str - 1 ∨ i ≥ Zlength str - 1) by omega.
            Caseeq Hi.
            {
              intros Hirange.
              unfold cons_buf_mid.
              assert (Hip1: 0 ≤ (i + 1) ≤ Zlength str - 1) by omega.
              repeat rewrite zle_le_true by omega. repeat rewrite zle_true by omega.
              solve_list.
              generalize (@skip_cons_n Z (Z.to_nat i) stl z). repeat toNat.
              intros Hss. rewrite Hss in H1. rewrite <- H0 in H1.
              solve_list. reflexivity.
            }
            {
              rewrite H0. solve_list. toZ. intros Hirange.
              assert (Hinat: ((Z.to_nat i) ≥ length stl)%nat).
              {
                repeat toZ. assumption. omega.
              }
              solve_list.
            }
          Qed.

          Lemma handle_cons_buf_eq_mid_overflow:
            ∀ i stl z x tlstl,
              0 ≤ i →
              i ≥ Zlength str - 1 →
              str = z :: stl →
              skipn (Z.to_nat i) stl = x :: tlstl →
              False.
          Proof.
            intros. generalize H0. intros.
            assert (H´´: ((Z.to_nat i) ≥ length stl)%nat).
            {
              repeat toZ. generalize H3. rewrite H1. rewrite Zlength_cons. intros. omega. omega.
            }
            solve_list.
          Qed.

          Lemma handle_cons_buf_eq_mid_sufficient:
            ∀ i stl z x tlstl,
              0 ≤ i ≤ Zlength str - 1 →
              i + Zlength (cons_buf cd) + 1 < CONS_BUFFER_MAX_DW →
              str = z :: stl →
              skipn (Z.to_nat i) stl = x :: tlstl →
              handle_cons_buf_write
                {| cons_buf := cons_buf_mid i; rpos := rpos_mid i |} x =
              {| cons_buf := cons_buf_mid (i + 1); rpos := rpos_mid (i + 1) |}.
          Proof.
            intros.
            unfold handle_cons_buf_write; simpl. rewrite zlt_true.
            unfold update_cons_buf; simpl.
            rewrite (cons_buf_mid_succ_still z stl x tlstl i); auto; try omega.
            rewrite (rpos_mid_succ_still); auto; try omega.
            apply cons_buf_mid_lt_max_dw; omega.
          Qed.

          Lemma handle_cons_buf_eq_mid_overlap:
            ∀ i stl z x tlstl,
              0 ≤ i < Zlength str - 1 →
              i + Zlength (cons_buf cd) + 1 > CONS_BUFFER_MAX_CHARS →
              str = z :: stl →
              skipn (Z.to_nat i) stl = x :: tlstl →
              handle_cons_buf_write
                {| cons_buf := cons_buf_mid i; rpos := rpos_mid i |} x =
              {| cons_buf := cons_buf_mid (i + 1); rpos := rpos_mid (i + 1) |}.
          Proof.
            intros.
            unfold handle_cons_buf_write.
            rewrite zlt_false; [| apply eq_imply_le; apply cons_buf_mid_eq_max_dw; omega].
            unfold update_cons_buf, update_rpos.
            remember 1%nat as n. simpl.
            unfold cons_buf_mid, rpos_mid.
            remember (Zlength str) as ls. remember (Zlength (cons_buf cd )) as lb.
            repeat rewrite zle_le_true by omega.
            repeat rewrite zle_false by omega.
            repeat toNat.
            remember (Z.to_nat i) as m.
            rewrite (skipn_firstnp1 (S m) str tlstl x).
            rewrite app_assoc.
            remember (cons_buf cd ++ firstn (S m) str) as lx. simpl.
            replace (Z.to_nat (i + 1 + 1 + lb)) with (S (Z.to_nat (i + 1 + lb))).
            remember (Z.to_nat (i + 1 + lb)) as p.
            assert (Hx: skipn n (skipn (p - 511) lx ++ x :: nil) = (skipn (S p - 511) (lx ++ x :: nil))).
            {
              assert (Hxi: skipn (p - 511) lx ++ x :: nil = skipn (p - 511) (lx ++ x :: nil)).
              {
                rewrite skipn_ge_tail. reflexivity.
                subst. toZ. repeat solve_list. rewrite min_l. repeat toZ; try omega.
                apply list_tl_eq in H1.
                rewrite H1. simpl.
                apply le_n_S. repeat toZ; try omega.
                generalize H. rewrite H1. solve_list. toZ. intros. omega.
              }
              rewrite Hxi. rewrite skipn_skipn. rewrite Heqn.
              replace (1 + (p - 511))%nat with (S p - 511)%nat. reflexivity.
              simpl. rewrite (NPeano.Nat.sub_succ_r p 510). unfold pred.
              destruct (p - 510)%nat eqn: Hp.
              - generalize H0, Hp. rewrite Heqp. simpl. intros.
                assert (Hfalse: i + lb + 1 = 510).
                {
                  apply Nat2Z.inj_iff in Hp0. generalize Hp0. repeat toZ. intros. omega.
                  omega. omega. omega.
                }
                rewrite Hfalse in H3. inversion H3.
              - reflexivity.
            }
            assert (Hy: ((rpos cd + lb + i + 2) mod 512 + 1) mod 512 = (rpos cd + lb + (i + 1) + 2) mod 512).
            {
              remember (rpos cd + lb) as a.
              replace (a + (i + 1) + 2) with ((a + i + 2) + 1) by omega.
              remember (a + i + 2) as b.
              rewrite Z.add_mod.
              assert (H1m512: 1 mod 512 = 1). rewrite Z.mod_small. reflexivity. omega.
              rewrite H1m512. rewrite Z.mod_mod.
              rewrite Z.add_mod with (a:=b) (b:=1). rewrite H1m512. reflexivity. omega. omega.
              omega.
            }
            rewrite Hy. f_equal.
            subst p. subst m.
            replace (Z.to_nat (i + 1 + lb) - 511)%nat with (Z.to_nat i + Z.to_nat lb - 510)%nat in Hx.
            rewrite Hx.
            replace (S (Z.to_nat (i + 1 + lb)) - 511)%nat with (Z.to_nat i + Z.to_nat lb - 509)%nat.
            reflexivity.
            repeat toNat. omega.
            repeat toNat. omega.
            repeat toNat. omega.
            rewrite H1. simpl. assumption.
          Qed.

          Lemma handle_cons_buf_eq_mid_dw:
            ∀ i stl z x tlstl,
              0 ≤ i < Zlength str - 1 →
              i + Zlength (cons_buf cd) + 1 = CONS_BUFFER_MAX_DW →
              str = z :: stl →
              skipn (Z.to_nat i) stl = x :: tlstl →
              handle_cons_buf_write
                {| cons_buf := cons_buf_mid i; rpos := rpos_mid i |} x =
              {| cons_buf := cons_buf_mid (i + 1); rpos := rpos_mid (i + 1) |}.
          Proof.
            intros.
            unfold handle_cons_buf_write. unfold update_cons_buf, update_rpos.
            remember 1%nat as n. simpl.
            unfold cons_buf_mid, rpos_mid; simpl.
            assert (H0´: i + 1 + Zlength (cons_buf cd) = CONS_BUFFER_MAX_DW) by omega.
            assert (H0´´: i + 1 + 1 + Zlength (cons_buf cd) = CONS_BUFFER_MAX_CHARS) by omega.
            assert (H0´´´ : Zlength (cons_buf cd) + i + 1 = CONS_BUFFER_MAX_DW) by omega.
            assert (H0´´´´ : Zlength (cons_buf cd) + (i + 1) + 1 = CONS_BUFFER_MAX_CHARS) by omega.
            assert (H´: 0 ≤ i + 1 ≤ Zlength str - 1) by omega.
            rewrite H0´, H0´´, H0´´´, H0´´´´. simpl.
            rewrite zlt_true.
            - rewrite zle_le_true by omega.
              rewrite zle_le_true by omega.
              replace ((cons_buf cd ++ firstn (Z.to_nat i + 1) str) ++ x :: nil) with
              (cons_buf cd ++ firstn (Z.to_nat (i + 1) + 1) str). reflexivity.
              {
                subst. rewrite H1. repeat toNat. repeat solve_list. reflexivity.
              }
            - rewrite zle_le_true by omega.
              repeat solve_list. rewrite min_l. repeat toZ; omega.
              repeat toZ; omega.
          Qed.

          Lemma handle_cons_buf_eq_mid_chars:
            ∀ i stl z x tlstl,
              0 ≤ i < Zlength str - 1 →
              i + Zlength (cons_buf cd) + 1 = CONS_BUFFER_MAX_CHARS →
              str = z :: stl →
              skipn (Z.to_nat i) stl = x :: tlstl →
              handle_cons_buf_write
                {| cons_buf := cons_buf_mid i; rpos := rpos_mid i |} x =
              {| cons_buf := cons_buf_mid (i + 1); rpos := rpos_mid (i + 1) |}.
          Proof.
            intros.
            unfold handle_cons_buf_write. unfold update_cons_buf, update_rpos.
            remember 1%nat as n. simpl.
            unfold cons_buf_mid, rpos_mid; simpl.
            assert (H0´: i + 1 + Zlength (cons_buf cd) = CONS_BUFFER_MAX_CHARS) by omega.
            assert (H0´´: i + 1 + 1 + Zlength (cons_buf cd) = CONS_BUFFER_SIZE) by omega.
            assert (H0´´´ : Zlength (cons_buf cd) + i + 1 = CONS_BUFFER_MAX_CHARS) by omega.
            assert (H0´´´´ : Zlength (cons_buf cd) + (i + 1) + 1 = CONS_BUFFER_SIZE) by omega.
            assert (H´: 0 ≤ i + 1 ≤ Zlength str - 1) by omega.
            rewrite H0´, H0´´, H0´´´, H0´´´´. replace (Z.to_nat (512 - 511)) with n by omega. simpl.
            rewrite zlt_false.
            - rewrite zle_le_true by omega.
              rewrite zle_le_true by omega.
              rewrite zle_le_true by omega.
              replace ((rpos cd + Zlength (cons_buf cd) + (i + 1) + 2)) with
              ((rpos cd + 513)) by omega.
              replace ((rpos cd + 513) mod 512) with ((rpos cd + 1) mod 512).
              replace ((cons_buf cd ++ firstn (Z.to_nat i + 1) str) ++ x :: nil) with
              (cons_buf cd ++ firstn (Z.to_nat (i + 1) + 1) str). reflexivity.
              {
                subst. repeat toNat. rewrite H1. repeat solve_list. reflexivity.
              }
              {
                rewrite Z.add_mod with (b:=513). replace (513 mod 512) with 1 by (compute; trivial).
                rewrite Z.mod_small with (a:= rpos cd) by omega. reflexivity. omega.
              }
            - rewrite zle_le_true by omega.
              repeat solve_list. rewrite min_l. repeat toZ; omega.
              repeat toZ; omega.
          Qed.

          Lemma handle_cons_buf_eq_mid:
            ∀ {i} {z} {stl} {x} {tlstl},
              0 ≤ i →
              str = z :: stl →
              skipn (Z.to_nat i) stl = x :: tlstl →
              handle_cons_buf_write
                {| cons_buf := cons_buf_mid i; rpos := rpos_mid i |} x =
              {| cons_buf := cons_buf_mid (i + 1); rpos := rpos_mid (i + 1) |}.
          Proof.
            remember (Zlength str) as ls. remember (Zlength (cons_buf cd) + 1) as lc.
            intros i z stl x tlstl Hi Hs Hstl.
            assert (Hiz: 0 ≤ i < ls - 1 ∨ i ≥ ls - 1) by omega; rewrite Heqls in Hiz.
            destruct Hiz.
            assert (Hic: i + lc < CONS_BUFFER_MAX_DW
                         ∨ i + lc > CONS_BUFFER_MAX_CHARS
                         ∨ i + lc = CONS_BUFFER_MAX_DW
                         ∨ i + lc = CONS_BUFFER_MAX_CHARS) by omega; rewrite Heqlc in Hic.
            - destruct Hic as [Hic | [Hic | [Hic | Hic]]].
              + apply (handle_cons_buf_eq_mid_sufficient i stl z x tlstl); try assumption; try omega.
              + apply (handle_cons_buf_eq_mid_overlap i stl z x tlstl); try assumption; try omega.
              + apply (handle_cons_buf_eq_mid_dw i stl z x tlstl); try assumption; try omega.
              + apply (handle_cons_buf_eq_mid_chars i stl z x tlstl); try assumption; try omega.
            - generalize (handle_cons_buf_eq_mid_overflow i stl z x tlstl Hi H Hs Hstl); inversion 1.
          Qed.

          Lemma rpos_overflow:
            ∀ {z} {stl},
              str = z :: stl →
              rpos_mid (Zlength stl) = rpos_mid (Z.succ (Zlength stl)).
          Proof.
            intros. unfold rpos_mid.
            assert (Hs: Zlength stl = Zlength str - 1).
            {
              rewrite H. solve_list. omega.
            }
            rewrite Hs.
            remember (Zlength str) as ls.
            remember (Zlength (cons_buf cd)) as lb.
            replace (Z.succ (ls - 1)) with ls by omega.
            assert (Hcb: lb + ls - 1 < CBL_MAX_CHARS
                         ∨ lb + ls - 1 = CBL_MAX_CHARS
                         ∨ lb + ls - 1 > CBL_MAX_CHARS) by omega.
            destruct Hcb as [Hcb | [Hcb | Hcb]].
            {
              rewrite zle_true by omega.
              rewrite zle_true by omega.
              reflexivity.
            }
            {
              rewrite zle_true by omega.
              rewrite zle_false by omega.
              case_if. omega.
              replace (rpos cd + lb + ls + 1) with (rpos cd + 512) by omega.
              rewrite Z.add_mod. rewrite Z.mod_same. rewrite Z.add_0_r. rewrite Z.mod_mod. rewrite Z.mod_small.
              reflexivity. omega. omega. omega. omega.
            }
            {
              rewrite zle_false by omega.
              rewrite zle_le_true.
              rewrite zle_false by omega.
              case_if. omega.
              replace (rpos cd + lb + (ls - 1) + 2) with (rpos cd + lb + ls + 1) by omega. reflexivity.
              rewrite <- Hs. generalize (Zlength_ge_0 stl). intros. omega.
            }
          Qed.

          Lemma cons_buf_overflow:
            ∀ {z} {stl},
              str = z :: stl →
              cons_buf_mid (Zlength stl) = cons_buf_mid (Z.succ (Zlength stl)).
          Proof.
            intros. unfold cons_buf_mid.
            assert (Hs: Zlength stl = Zlength str - 1).
            {
              rewrite H. solve_list. omega.
            }
            rewrite Hs. generalize (Zlength_ge_0 stl); intros Hstl.
            remember (Zlength str) as ls.
            remember (Zlength (cons_buf cd)) as lb.
            replace (Z.succ (ls - 1)) with ls by omega.
            rewrite zle_le_true by omega.

            assert (Hcb: lb + ls < CONS_BUFFER_MAX_CHARS
                         ∨ lb + ls = CONS_BUFFER_MAX_CHARS
                         ∨ lb + ls > CONS_BUFFER_MAX_CHARS) by omega.
            destruct Hcb as [Hcb | [Hcb | Hcb]].
            {
              rewrite zle_true.
              case_if. omega.
              rewrite zle_true.
              replace ((Z.to_nat (ls - 1) + 1)%nat) with (Z.to_nat ls).
              subst. rewrite Zlength_correct. rewrite Nat2Z.id. repeat solve_list. reflexivity.
              rewrite Z2Nat.inj_sub. toNat. rewrite x_s1_p1_0. reflexivity.
              repeat toZ; omega. omega. omega. omega.
            }
            {
              rewrite zle_true by omega.
              case_if. omega.
              rewrite zle_false by omega.
              replace (Z.to_nat (ls - 1) + 1)%nat with (Z.to_nat ls).
              replace (ls + lb - CONS_BUFFER_MAX_CHARS) with 0 by omega.
              toNat. subst. rewrite Zlength_correct. rewrite Nat2Z.id. repeat solve_list. reflexivity.

              rewrite Z2Nat.inj_sub. toNat. rewrite x_s1_p1_0. reflexivity.
              repeat toZ; omega. omega.
            }
            {
              rewrite zle_false by omega.
              case_if. omega.
              rewrite zle_false by omega.
              replace (ls - 1 + 1 + lb - CONS_BUFFER_MAX_CHARS) with (ls + lb - CONS_BUFFER_MAX_CHARS) by omega.
              replace (Z.to_nat (ls - 1) + 1)%nat with (Z.to_nat ls).
              replace (Z.to_nat ls) with (length str).
              solve_list. reflexivity.
              rewrite Heqls. rewrite Zlength_correct. rewrite Nat2Z.id. reflexivity.
              rewrite Z2Nat.inj_sub. toNat. rewrite x_s1_p1_0. reflexivity.
              repeat toZ; omega. omega.
            }
          Qed.


          Section RxBufNotEmpty.

            Variable ht: Z.
            Variable tlt: list Z.
            Hypothesis Hot: t = ht :: tlt.

            Lemma cons_intr_loop_correct_aux_ne:
              LoopProofSimpleWhile.t
                cons_intr_loop_condition
                cons_intr_loop_body
                ge (PTree.empty _)
                cons_intr_loop_body_P
                cons_intr_loop_body_Q.
            Proof.
              generalize max_unsigned_val; intro muval.
              assert (Zlength str > 0).
              {
                rewrite Hos. rewrite Zlength_cons. generalize (Zlength_ge_0 t). intros. omega.
              }
              assert (Zlength t > 0).
              {
                rewrite Hot. rewrite Zlength_cons. generalize (Zlength_ge_0 tlt). intros. omega.
              }
              apply LoopProofSimpleWhile.make with
              (W := Z)
                (lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
                (I := fun le m w ⇒ ∃ i,
                                  le ! _t = Some (Vint (Int.repr i)) ∧
                                  w = Zlength str - i ∧
                                  ((
                                      0 ≤ i ≤ Zlength t ∧
                                      le ! _hasMore = Some (Vint (Int.one)) ∧
                                      m = (m_init, abd {com1 / l1: (l1 (com1 abd)) + i × 2}
                                                        {com1 / s / RxBuf: skipn (S (Z.to_nat i)) str}
                                                        {console / cons_buf: cons_buf_mid i}
                                                        {console / rpos: rpos_mid i})
                                    ) ∨ (
                                     i = Zlength t + 1 ∧
                                     le ! _hasMore = Some (Vint (Int.zero)) ∧
                                     m = (m_init, d_end)
                                   ))
                ).
              apply Zwf_well_founded.
              intros le m Hp.
              destruct Hp as (Hplehas & Hplet & Hpm).
              ∃ (Zlength str), 0.
              rewrite Hpm. rewrite Z.add_0_r; unfold update_ts; simpl.
              destruct abd; simpl.
              repeat constructor; discharge_cmp.
              unfold_all.
              rewrite Hos.
              destruct abd; simpl. destruct com1; simpl. destruct s eqn: Hs; simpl.
              repeat constructor; discharge_cmp; simpl in *; subst.
              reflexivity.

              unfold cons_intr_loop_body_Q. unfold d_end.
              unfold_all.
              destruct abd; destruct com1; destruct s; destruct console; simpl in ×.
              subst str. rewrite Hot in ×. generalize (forall_tl Hschar); intros Hosstl.
              generalize (forall_tl Hosstl); intros Hottl.
              intros le m w Hi.
              destruct Hi as (i & Hlet & Hn & [Hcontinue | Hbreak]).
              - Case ("continue").
                destruct Hcontinue as (Hi & Hlemore & Hm).
                rewrite Zlength_cons in ×.
                assert (Hirange´´: 0 ≤ i < Zlength t ∨ i = Zlength t).
                {
                  rewrite Hot. rewrite Zlength_cons. omega.
                }
                Caseeq (Hirange´´).
                {
                  intros Hreali.
                  assert (Hskipi: ∃ sith sittl, skipn (Z.to_nat i) (ht :: tlt) = sith :: sittl).
                  {
                    rewrite <- Hot.
                    apply non_nil_list.
                    generalize (Zlength_lt i t Hreali); intros Hnati.
                    generalize (skipn_lt t (Z.to_nat i) Hnati); intros Hsinnil.
                    assumption.
                  }
                  destruct Hskipi as (sith & sittl & Hskipi).
                  assert (Hskipix: skipn (Z.to_nat i) tlt = sittl).
                  {
                    apply skipn_less in Hskipi. assumption.
                  }
                  assert (Hskipirange: isChar sith).
                  {
                    rewrite <- Hot in ×.
                    generalize (@forall_skipn_hd_erange t (Z.to_nat i) sith sittl Hosstl Hskipi); auto.
                  }
                  assert (Hrealitlt: 0 ≤ i < Z.succ (Zlength tlt)).
                  {
                    rewrite Hot in Hreali. rewrite Zlength_cons in Hreali. assumption.
                  }
                  repeat rewrite Zlength_cons in ×.
                  unfold isChar in ×.
                  esplit. esplit.
                  split; [| split; [| split]].
                  + SCase ("loop condition").
                    unfold cons_intr_loop_condition.
                    repeat vcgen.
                  + SCase ("bool val = true").
                    repeat vcgen.
                  + SCase ("not done").
                    inversion 1.
                  + SCase ("will continue").
                    intros Htrivial; clear Htrivial.
                    esplit. esplit.
                    split.
                    × SSCase ("execute loop body").
                      unfold cons_intr_loop_body.
                      repeat vcgen.
                      unfold serial_getc_spec; simpl.
                      rewrite Hserex; simpl.
                      rewrite Hkern, Hinit, Hhost, Hon, HrxIntMask, Hdlab, Hskipi.
                      if_true.
                      rewrite (Hevents (i × 2)).
                      replace (l1 + i × 2 + 1) with (l1 + (i × 2 + 1)) by omega. rewrite (Hevents (i × 2 + 1)).
                      unfold_all.
                      rewrite Int.unsigned_repr.
                      reflexivity.
                      omega. omega. omega.
                    × ∃ (Zlength t - i).
                      split.
                      - SSCase ("loop index reduction").
                        subst w. split. omega. subst t. rewrite Zlength_cons. omega.
                      - SSCase ("loop invariants hold").
                        ∃ (i + 1).
                        split; [| split].
                        repeat vcgen. subst t. rewrite Zlength_cons. omega.
                        left.
                        split; [| split].
                        omega.
                        repeat vcgen.
                        replace (l1 + (i + 1) × 2) with (l1 + i × 2 + 2) by omega.
                        repeat toNat. simpl.
                        rewrite Hkern, Hinit, Hhost, Hon, HrxIntMask, Hdlab, HserIntr, Hskipix.
                        rewrite (@handle_cons_buf_eq_mid i h t sith sittl); try assumption; try omega.
                        reflexivity. subst. reflexivity. subst t. assumption.
                }
                {
                  intros Hreali; rewrite Hreali in ×.
                  rewrite <- Hot in ×.
                  unfold isChar in ×.
                  esplit. esplit.
                  split; [| split; [| split]].
                  + SCase ("loop condition").
                    unfold cons_intr_loop_condition.
                    repeat vcgen.
                  + SCase ("bool val = true").
                    repeat vcgen.
                  + SCase ("not done").
                    inversion 1.
                  + SCase ("will continue").
                    intros Htrivial; clear Htrivial.
                    esplit. esplit.
                    split.
                    × SSCase ("execute loop body").
                      unfold cons_intr_loop_body.
                      repeat vcgen.
                      rewrite zlength_to_length. rewrite skipn_length.
                      unfold serial_getc_spec; simpl.
                      rewrite Hserex; simpl. rewrite Hreali; simpl.
                      rewrite Hkern, Hinit, Hhost, Hon, HrxIntMask, Hdlab, HserIntr.
                      rewrite (Hevents (Zlength t × 2)).
                      unfold_all.
                      rewrite Int.unsigned_repr. reflexivity.
                      omega. omega.
                    × ∃ (0).
                      split.
                      - SSCase ("loop index reduction").
                        split. omega. omega.
                      - SSCase ("loop invariants hold").
                        ∃ (Zlength t + 1).
                        split; [| split].
                        repeat vcgen. rewrite Zlength_cons. omega.
                        right.
                        split; [| split].
                        rewrite Hot. rewrite Zlength_cons. omega.
                        repeat vcgen.
                        rewrite Zlength_cons.
                        rewrite <- (@rpos_overflow h t Hos).
                        rewrite <- (@cons_buf_overflow h t Hos).
                        rewrite Hkern, Hinit, Hhost, Hon, HrxIntMask, Hdlab, HserIntr.
                        replace (l1 + Zlength t × 2 + 1) with (l1 + Z.succ (Zlength tlt) × 2 + 1).
                        reflexivity.
                        rewrite Hot. rewrite Zlength_cons. omega.
                }
              - Case "break".
                rewrite <- Hot in ×. rewrite <- Hos in ×.
                destruct Hbreak as (Hi & Hmore & Hm).
                esplit. esplit. rewrite Hi in ×.
                split; [| split; [| split]].
                + SCase "loop condition".
                  unfold cons_intr_loop_condition.
                  repeat vcgen. generalize Hslen. rewrite Hos. rewrite Zlength_cons. intros. omega.
                + SCase "bool val = false".
                  repeat vcgen.
                + SCase "done".
                  intros Htrivial; clear Htrivial.
                  unfold cons_intr_loop_body_Q. rewrite Hm. unfold d_end.
                  unfold_all. reflexivity.
                + SCase "not continue".
                  inversion 1.
            Qed.

          End RxBufNotEmpty.

          Section RxBufIsEmpty.

            Hypothesis Hot: t = nil.

            Lemma cons_intr_loop_correct_aux_e:
              LoopProofSimpleWhile.t
                cons_intr_loop_condition
                cons_intr_loop_body
                ge (PTree.empty _)
                cons_intr_loop_body_P
                cons_intr_loop_body_Q.
            Proof.
              generalize max_unsigned_val; intro muval.
              assert (Zlength str > 0).
              {
                rewrite Hos. rewrite Zlength_cons. generalize (Zlength_ge_0 t). intros. omega.
              }
              assert (Zlength t = 0).
              {
                rewrite Hot. rewrite Zlength_nil. reflexivity.
              }
              apply LoopProofSimpleWhile.make with
              (W := Z)
                (lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
                (I := fun le m w ⇒ ∃ i,
                                  le ! _t = Some (Vint (Int.repr i)) ∧
                                  w = Zlength str - i ∧
                                  ((
                                      0 ≤ i ≤ Zlength t ∧
                                      le ! _hasMore = Some (Vint (Int.one)) ∧
                                      m = (m_init, abd {com1 / l1: (l1 (com1 abd)) + i × 2}
                                                        {com1 / s / RxBuf: skipn (S (Z.to_nat i)) str}
                                                        {console / cons_buf: cons_buf_mid i}
                                                        {console / rpos: rpos_mid i})
                                    ) ∨ (
                                     i = Zlength t + 1 ∧
                                     le ! _hasMore = Some (Vint (Int.zero)) ∧
                                     m = (m_init, d_end)
                                   ))
                ).
              apply Zwf_well_founded.
              intros le m Hp.
              destruct Hp as (Hplehas & Hplet & Hpm).
              ∃ (Zlength str), 0.
              rewrite Hpm. rewrite Z.add_0_r; unfold update_ts; simpl.
              destruct abd; simpl.
              repeat constructor; discharge_cmp.
              unfold_all.
              rewrite Hos.
              destruct abd; simpl. destruct com1; simpl. destruct s eqn: Hs; simpl.
              repeat constructor; discharge_cmp; simpl in *; subst.
              reflexivity.

              unfold cons_intr_loop_body_Q. unfold d_end.
              unfold_all.
              destruct abd; destruct com1; destruct s; destruct console; simpl in ×.
              subst str. rewrite Hot in ×. generalize (forall_tl Hschar); intros Hosstl.
              intros le m w Hi.
              destruct Hi as (i & Hlet & Hn & [Hcontinue | Hbreak]).
              - Case ("continue").
                destruct Hcontinue as (Hi & Hlemore & Hm).
                assert (Hreali: i = 0) by omega.
                {
                  unfold isChar in ×.
                  esplit. esplit.
                  split; [| split; [| split]].
                  + SCase ("loop condition").
                    unfold cons_intr_loop_condition.
                    repeat vcgen.
                  + SCase ("bool val = true").
                    repeat vcgen.
                  + SCase ("not done").
                    inversion 1.
                  + SCase ("will continue").
                    intros Htrivial; clear Htrivial.
                    esplit. esplit.
                    split.
                    × SSCase ("execute loop body").
                      unfold cons_intr_loop_body.
                      repeat vcgen.
                      unfold serial_getc_spec; simpl.
                      rewrite Hserex; simpl.
                      rewrite Hreali, Hkern, Hinit, Hhost, Hon, HrxIntMask, Hdlab, HserIntr. rewrite skipn_nil.
                      rewrite Z.mul_0_l.
                      rewrite (Hevents 0).
                      unfold_all.
                      rewrite Int.unsigned_repr. reflexivity.
                      omega. omega.
                    × ∃ (0).
                      rewrite Hreali in ×.
                      split.
                      - SSCase ("loop index reduction").
                        split. omega. omega.
                      - SSCase ("loop invariants hold").
                        ∃ (1).
                        split; [| split].
                        repeat vcgen. simpl. reflexivity.
                        right.
                        split; [| split].
                        simpl. reflexivity.
                        repeat vcgen.
                        rewrite Zlength_cons.
                        rewrite <- (@rpos_overflow h nil Hos).
                        rewrite <- (@cons_buf_overflow h nil Hos).
                        rewrite Hkern, Hinit, Hhost, Hon, HrxIntMask, Hdlab, HserIntr; simpl.
                        reflexivity.
                }
              - Case "break". simpl.
                destruct Hbreak as (Hi & Hmore & Hm).
                esplit. esplit. rewrite Hi in ×.
                split; [| split; [| split]].
                + SCase "loop condition".
                  unfold cons_intr_loop_condition.
                  repeat vcgen.
                + SCase "bool val = false".
                  repeat vcgen.
                + SCase "done".
                  intros Htrivial; clear Htrivial.
                  unfold cons_intr_loop_body_Q. rewrite Hm. unfold d_end.
                  unfold_all. reflexivity.
                + SCase "not continue".
                  inversion 1.
            Qed.
          End RxBufIsEmpty.

          Lemma cons_intr_loop_correct_aux:
            LoopProofSimpleWhile.t
              cons_intr_loop_condition
              cons_intr_loop_body
              ge (PTree.empty _)
              cons_intr_loop_body_P
              cons_intr_loop_body_Q.
          Proof.
            destruct t as [| z stl] eqn: Hstr.
            apply cons_intr_loop_correct_aux_e. assumption.
            apply (cons_intr_loop_correct_aux_ne z stl). assumption.
          Qed.

        End cons_intr_loop_proof.

        Lemma cons_intr_loop_correct:
          ∀ m d le str h t c cd,
            SerialEnv ((l1 (com1 d)) - 3) = SerialRecv (h :: t) →
            (RxBuf (s (com1 d))) = t →
            (TxBuf (s (com1 d))) = nil →
            (SerialOn (s (com1 d))) = true →
            (RxIntEnable (s (com1 d))) = true →
            (SerialIrq (s (com1 d))) = false →
            DLAB (s (com1 d)) = false →
            high_level_invariant d →
            ikern d = true →
            init d = true →
            ihost d = true →
            serial_exists (drv_serial d) = 1 →
            0 ≤ rpos cd < 512 →
            str = h :: t →
            last str 0 = c →
            Zlength str ≤ 12 →
            Forall isChar str →
            (∀ n : Z,
               n ≤ Zlength str × 2 + 2 → SerialEnv (l1 (com1 d) + n) = NullEvent) →
            console d = mkConsoleDrvier (cons_buf_mid str cd 0) (rpos_mid str cd 0) →
            le ! _hasMore = Some (Vint (Int.one)) →
            le ! _t = Some (Vint (Int.zero)) →
            ∃ le´, exec_stmt ge (PTree.empty _) le ((m, d): mem)
                             (Swhile cons_intr_loop_condition cons_intr_loop_body)
                             E0 le´ (m, (d_end d str t cd)) Out_normal.
        Proof.
          intros.
          generalize (cons_intr_loop_correct_aux m d str h t c cd H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H15 H16 H17).
          unfold cons_intr_loop_body_P, cons_intr_loop_body_Q.
          intro Hlp.
          refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ Hlp le (m, d) _)).
          intro pre.
          destruct pre as (le´ & m´ & Hexec & Hd_end).
          ∃ le´. subst. assumption.
          repeat split; try assumption.
        Qed.

        Lemma simp_cons_buf:
          ∀ c r,
            DeviceStateDataType.cons_buf ({|cons_buf := c; rpos := r|}) = c.
        Proof.
          intros. simpl. reflexivity.
        Qed.

        Lemma simp_rpos:
          ∀ c r,
            DeviceStateDataType.rpos ({|cons_buf := c; rpos := r|}) = r.
        Proof.
          intros. simpl. reflexivity.
        Qed.

        Lemma cons_intr_body_correct:
          ∀ m d d´ env le,
            env = PTree.empty _ →
            high_level_invariant d →
            cons_intr_aux d = Some d´ →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) cons_intr_real_body E0 le´ (m, d´)
                        Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros m d d´ env le Henv Hinv Hspec.
          inversion Hinv. generalize valid_cons_buf_rpos, valid_cons_buf_length.
          intros Hrpos Hconsbuf.
          functional inversion Hspec;
          (on_eq_right (d´) act (fun Hx ⇒ try rewrite <- Hx in *));
           (on_eq_left (zeq 1 (serial_exists (drv_serial d))) act (fun Hx ⇒ clear Hx));
           (on_eq_left (ihost d) act (fun Hx ⇒ rename Hx into Hhost));
           (on_eq_left (ikern d) act (fun Hx ⇒ rename Hx into Hkern));
           (on_eq_left (init d) act (fun Hx ⇒ rename Hx into Hinit));
           (on_eq_left (in_intr d) act (fun Hx ⇒ rename Hx into Hintr));
           (on_eq_right (serial_exists (drv_serial d)) act (fun Hx ⇒ rename Hx into Hserex));
           (on_eq_left (SerialEnv (lrx - 1)) act (fun Hx ⇒ rename Hx into Horacle));
           (on_eq_left (com1 d) act (fun Hx ⇒ rename Hx into Hs));
           subst;
           destruct d; destruct com1, drv_serial, console; subst;
           simpl in *; rewrite Hhost, Hkern, Hserex in *; simpl in *;
           unfold_all; clear Hspec;
           destruct s; inversion Hs; subst; simpl; clear Hs;
           simpl in *; generalize (OracleInvariants.serial_recv_limit (lrx - 1) rxbuf Horacle);
           intro Heit;
           destruct Heit as (Hsnnil & Hslen & Hschar & Hnop);
           generalize (non_nil_list Hsnnil); intros Hsnnilex; destruct Hsnnilex as (h & t & Hsex); subst;
           inversion Hschar; unfold isChar in ×.

           -
             assert (Hcrange: Zlength (cons_buf) < 511).
             {
               generalize _x10. solve_list. intros.
               generalize (Zlength_ge_1 h t). intros. omega.
             }
             assert (Hcsrange: Zlength(cons_buf) + Zlength(h :: t) ≤ 511).
             {
               generalize _x10. solve_list. auto.
             }
             assert (Hnop´: ∀ n : Z,
                              n ≤ Zlength (h :: t) × 2 + 4 → SerialEnv (lrx + n) = NullEvent).
             {
               intros; generalize (Hnop (n+1));
               replace (lrx - 1 + (n + 1)) with (lrx + n) by omega;
               intros Htmp; apply Htmp; omega.
             }

             remember ({| cons_buf := cons_buf; rpos := rpos |}) as cd.
             exec_pre_abd preabd.
             remember (preabd {com1 / s / SerialIrq: false}
                              {com1 / s / RxBuf: l}
                              {com1 / l1: lrx + 2}
                              {console / cons_buf: cons_buf ++ h :: nil}) as dl.
             generalize Heqdl. unfold_RData. unfold_DeviceData. unfold_SerialState.
               rewrite Heqcd. unfold update_cons_buf; simpl. clear Heqdl. intros Heqdl.
             subst preabd.
             remember ((PTree.set _t (Vint Int.zero)
                                  (PTree.set _hasMore (Vint Int.one) le))) as lel.
             exploit (cons_intr_loop_correct m dl lel (h :: t) h t (last (h :: t) 0) cd);
               try rewrite Heqdl; try rewrite Heqlel; try rewrite Heqcd;
               simpl; try auto; try omega; try discharge_cmp. rewrite <- Horacle.
             apply f_equal. omega.
             econstructor; eauto. simpl. repeat solve_list. simpl. omega.
             intros. generalize (Hnop´ (2 + n)). calc. intros Htmp. rewrite Htmp. reflexivity. omega.
             {
               unfold cons_buf_mid, rpos_mid. rewrite zle_le_true by omega.
               rewrite zle_true. simpl. rewrite zle_true. reflexivity.
               omega.
               replace (DeviceStateDataType.cons_buf {| cons_buf := cons_buf; rpos := rpos |}) with cons_buf
                 by (simpl; trivial).
               omega.
             }
             repeat vcgen. repeat vcgen.
             intros Hloop.
             destruct Hloop as (le_after_loop & Hloopexec).
             generalize Hloopexec; clear Hloopexec.
             unfold d_end. unfold update_cons_buf, update_rpos; simpl.
             unfold_all.
             replace (cons_buf_mid (h :: t) {| cons_buf := cons_buf; rpos := rpos |} (Zlength (h :: t)))
             with (cons_buf ++ h :: t).
             replace (rpos_mid (h :: t) {| cons_buf := cons_buf; rpos := rpos |} (Zlength (h :: t)))
             with rpos.
             replace (ts + 2 + Zlength (h :: t) × 2 - 1) with (ts + Zlength (h :: t) × 2 + 1) by omega.
             intros Hloopexec.
             esplit; unfold cons_intr_body.
             repeat vcgen.
             unfold serial_getc_spec; subst; simpl.
             rewrite zle_le_true by omega.
             generalize (Hnop´ 0). rewrite Z.add_0_r. intros Htmp. rewrite Htmp. clear Htmp.
             rewrite (Hnop´ 1).
             unfold_all.
             rewrite Int.unsigned_repr.
             replace (handle_cons_buf_write {| cons_buf := cons_buf; rpos := rpos |} h) with
             {| cons_buf := cons_buf ++ h :: nil; rpos := rpos |}.
             reflexivity.
             {
               unfold handle_cons_buf_write. rewrite zlt_true.
               unfold update_cons_buf; simpl. reflexivity.
               simpl. omega.
             }
             omega. omega. omega.
             discharge_cmp. simpl. repeat vcgen. rewrite Heqdl.
             rewrite Zlength_cons. replace (lrx + Z.succ (Zlength t) × 2 + 1) with (lrx + 2 + Zlength t × 2 + 1) by omega.