Library mcertikos.invariants.INVLemmaDriver

Require Import Coqlib.
Require Import Maps.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import FutureTactic.
Require Import AuxLemma.
Require Import DeviceStateDataType.
Require Import AbstractDataType.

Require Import Values.
Require Import AsmX.
Require Import Integers.
Require Import liblayers.compat.CompatLayers.
Require Import AST.
Require Import OracleInstances.
Require Import XOmega.

Open Scope Z_scope.

Section CONSOLE_INV.

  Require Import ObjConsole.

  Lemma handle_cons_buf_write_reserve_rpos:
    ∀ d c,
      0 ≤ rpos (console d) < CONSOLE_BUFFER_SIZE →
      0 ≤ rpos (handle_cons_buf_write (console d) c) < CONSOLE_BUFFER_SIZE.
  Proof.
    intros. unfold handle_cons_buf_write.
    case_if.
    unfold_console; assumption.
    unfold_console. apply Z_mod_lt; omega.
  Qed.

  Lemma handle_cons_buf_write_reserve_cons_buf_len:
    ∀ d c,
      0 ≤ Zlength (cons_buf (console d)) < CONSOLE_BUFFER_SIZE →
      0 ≤ Zlength (cons_buf (handle_cons_buf_write (console d) c)) < CONSOLE_BUFFER_SIZE.
  Proof.
    intros. unfold handle_cons_buf_write.
    case_if.
    unfold_console. repeat solve_list. simpl. omega.
    remember 1%nat as n. unfold_console.
    repeat solve_list. rewrite Heqn. simpl.
    repeat toZ; omega.
  Qed.

  Lemma cons_buf_plus_1_reserve_rpos:
  ∀ d len,
    0 ≤ rpos (console d) < len →
    0 ≤ (rpos (console d) + 1) mod len < len.
  Proof.
    intros. xomega.
  Qed.

  Lemma cons_buf_tl_reserve_cons_buf_len:
  ∀ z tl len,
    0 ≤ Zlength (Int.unsigned z :: tl) < len →
    0 ≤ Zlength tl < len.
  Proof.
    intros z tl len. solve_list. intros.
    split.
    - apply list_gt_0.
    - destruct H. apply succ_lt_lt. assumption.
  Qed.

  Lemma cons_buf_tl_cons_reserve_cons_buf_len:
  ∀ d z tl len,
    0 ≤ Zlength (cons_buf (console d)) < len →
    cons_buf (console d) = Int.unsigned z :: tl →
    0 ≤ Zlength tl < len.
  Proof.
    intros. rewrite H0 in H. apply cons_buf_tl_reserve_cons_buf_len with (z:=z).
    assumption.
  Qed.

  Lemma nil_zlength_within_range: 0 ≤ @Zlength Z nil < CONSOLE_BUFFER_SIZE.
  Proof.
    rewrite Zlength_nil. omega.
  Qed.

  Import DeviceStateDataType.
  Lemma cons_intr_preserves_cons_buf_len:
    ∀ d rxbuf,
      Zlength (cons_buf (console d) ++ rxbuf) ≤ CONSOLE_BUFFER_SIZE - 1 →
      0 ≤ Zlength (cons_buf (console d) ++ rxbuf) < CONSOLE_BUFFER_SIZE.
  Proof.
    intros. generalize (Zlength_ge_0 (cons_buf (console d) ++ rxbuf)). intros.
    omega.
  Qed.

  Lemma cons_intr_preserves_rpos_range:
    ∀ d rxbuf,
      0 ≤ (rpos (console d) + Zlength (cons_buf (console d) ++ rxbuf) + 1)
             mod CONSOLE_BUFFER_SIZE < CONSOLE_BUFFER_SIZE.
  Proof.
    intros. apply Z_mod_lt; omega.
  Qed.

  Lemma cons_intr_skipn_reserve_cons_buf_len:
    ∀ d rxbuf,
      0 ≤ Zlength (cons_buf (console d)) < CONSOLE_BUFFER_SIZE →
      Zlength (cons_buf (console d) ++ rxbuf) > CONSOLE_BUFFER_SIZE - 1 →
      0 ≤ Zlength
             (skipn (Z.to_nat (Zlength (cons_buf (console d) ++ rxbuf) - 511))
                    (cons_buf (console d) ++ rxbuf)) < CONSOLE_BUFFER_SIZE.
  Proof.
    intros. repeat solve_list. repeat toZ; try omega;
                               generalize H0; repeat solve_list; intros; omega.
  Qed.

End CONSOLE_INV.
Section IOAPIC_INV.

  Require Import ObjInterruptController.

  Lemma ioapic_trans_intr_reserves_maxintr:
    ∀ s s´ w,
      ioapic_trans_intr w s = s´ →
      IoApicMaxIntr s = IoApicMaxIntr s´.
  Proof.
    intros. repeat (iinv s); subst; unfold_IoApicState; auto.
  Qed.

  Lemma ioapic_trans_intr_reserves_maxintr_simpl:
    ∀ s w,
      IoApicMaxIntr (ioapic_trans_intr w s) = IoApicMaxIntr s.
  Proof.
    intros. erewrite <- ioapic_trans_intr_reserves_maxintr; reflexivity.
  Qed.

  Lemma ioapic_trans_intr_reserves_enables_length:
    ∀ s s´ w,
      ioapic_trans_intr w s = s´ →
      Zlength (IoApicEnables s) = Zlength (IoApicEnables s´).
  Proof.
    intros. repeat (iinv s); subst; unfold_IoApicState; auto.
  Qed.

  Lemma ioapic_trans_intr_reserves_enables_length_simpl:
    ∀ s w,
      Zlength (IoApicEnables (ioapic_trans_intr w s)) = Zlength (IoApicEnables s).
  Proof.
    intros. erewrite <- ioapic_trans_intr_reserves_enables_length; reflexivity.
  Qed.

  Lemma ioapic_trans_intr_reserves_irqs_length:
    ∀ s s´ w,
      ioapic_trans_intr w s = s´ →
      Zlength (IoApicIrqs s) = Zlength (IoApicIrqs s´).
  Proof.
    intros. repeat (iinv s); subst; unfold_IoApicState; auto.
  Qed.

  Lemma ioapic_trans_intr_reserves_irqs_length_simpl:
    ∀ s w,
      Zlength (IoApicIrqs (ioapic_trans_intr w s)) = Zlength (IoApicIrqs s).
  Proof.
    intros. erewrite <- ioapic_trans_intr_reserves_irqs_length; reflexivity.
  Qed.

  Lemma ioapic_trans_intr_reserves_irqs:
    ∀ s w,
      IoApicIrqs (ioapic_trans_intr w s) = IoApicIrqs s.
  Proof.
    intros. remember (ioapic_trans_intr w s) as s´.
    repeat (iinv s); subst; unfold_IoApicState; auto.
  Qed.

  Lemma ioapic_trans_intr_reserves_maxintr_within_range:
    ∀ d w,
      0 ≤ IoApicMaxIntr (s (ioapic d)) < 32 →
      0 ≤ IoApicMaxIntr (ioapic_trans_intr w (s (ioapic d))) < 32.
  Proof.
    intros. remember (s (ioapic d)) as s.
    remember (ioapic_trans_intr w s) as s´.
    generalize (ioapic_trans_intr_reserves_maxintr s s´ w). intros Heq.
    rewrite <- ioapic_trans_intr_reserves_maxintr with (s:=s)(w:=w). assumption.
    subst. reflexivity.
  Qed.

  Lemma ioapic_trans_cpu_reserves_maxintr:
    ∀ s s´ o,
      ioapic_trans_cpu o s = s´ →
      IoApicMaxIntr s = IoApicMaxIntr s´.
  Proof.
    intros. repeat (iinv s); subst; unfold_IoApicState; auto.
  Qed.

  Lemma ioapic_trans_cpu_reserves_maxintr_simpl:
    ∀ s w,
      IoApicMaxIntr (ioapic_trans_cpu w s) = IoApicMaxIntr s.
  Proof.
    intros. erewrite <- ioapic_trans_cpu_reserves_maxintr; reflexivity.
  Qed.

  Lemma ioapic_trans_cpu_reserves_enables_length:
    ∀ s s´ o,
      ioapic_trans_cpu o s = s´ →
      Zlength (IoApicEnables s) = Zlength (IoApicEnables s´).
  Proof.
    intros. repeat (iinv s); subst; unfold_IoApicState; auto.
    rewrite replace_preserves_Zlength; reflexivity.
  Qed.

  Lemma ioapic_trans_cpu_reserves_enables_length_simpl:
    ∀ s w,
      Zlength (IoApicEnables (ioapic_trans_cpu w s)) = Zlength (IoApicEnables s).
  Proof.
    intros. erewrite <- ioapic_trans_cpu_reserves_enables_length; reflexivity.
  Qed.

  Lemma ioapic_trans_cpu_reserves_irqs_length:
    ∀ s s´ o,
      ioapic_trans_cpu o s = s´ →
      Zlength (IoApicIrqs s) = Zlength (IoApicIrqs s´).
  Proof.
    intros. repeat (iinv s); subst; unfold_IoApicState; auto.
    rewrite replace_preserves_Zlength; reflexivity.
  Qed.

  Lemma ioapic_trans_cpu_reserves_irqs_length_simpl:
    ∀ s w,
      Zlength (IoApicIrqs (ioapic_trans_cpu w s)) = Zlength (IoApicIrqs s).
  Proof.
    intros. erewrite <- ioapic_trans_cpu_reserves_irqs_length; reflexivity.
  Qed.

  Lemma ioapic_trans_cpu_does_not_change_maxintr:
    ∀ s o,
      IoApicMaxIntr (ioapic_trans_cpu o s) = IoApicMaxIntr s.
  Proof.
    intros. symmetry. apply ioapic_trans_cpu_reserves_maxintr with (o:=o).
    reflexivity.
  Qed.

  Lemma ioapic_trans_cpu_reserves_maxintr_within_range:
    ∀ d o,
    0 ≤ IoApicMaxIntr (s (ioapic d)) < 32 →
    0 ≤ IoApicMaxIntr (ioapic_trans_cpu o (s (ioapic d))) < 32.
  Proof.
    intros. generalize (ioapic_trans_cpu_reserves_maxintr
                         (s (ioapic d))
                         (ioapic_trans_cpu o (s (ioapic d))) o).
    intros Heq. rewrite <- Heq. assumption. reflexivity.
  Qed.

  Require Import ObjInterruptDriver.
  Require Import ObjInterruptController.

  Lemma init_does_not_change_max_intr:
    ∀ n s,
      (IoApicMaxIntr (ioapic_init_aux s n)) = IoApicMaxIntr s.
  Proof.
    induction n.
    - simpl. trivial.
    - intros. simpl. rewrite IHn. trivial.
  Qed.

  Lemma init_does_not_change_enables_length:
    ∀ n s,
      Zlength (IoApicEnables (ioapic_init_aux s n)) = Zlength (IoApicEnables s).
  Proof.
    intros. induction n.
    - simpl. rewrite replace_preserves_Zlength; reflexivity.
    - simpl.
      remember (IoApicEnables (ioapic_init_aux s n)) as l.
      remember (Zlength (IoApicEnables s)) as n´.
      rewrite replace_preserves_Zlength. assumption.
  Qed.

  Lemma init_does_not_change_irqs_length:
    ∀ n s,
      Zlength (IoApicIrqs (ioapic_init_aux s n)) = Zlength (IoApicIrqs s).
  Proof.
    intros. induction n.
    - simpl. rewrite replace_preserves_Zlength. reflexivity.
    - remember (IoApicIrqs (ioapic_init_aux s n)) as l.
      remember (Zlength (IoApicIrqs s)) as n´.
      Opaque Z.add Z.of_nat.
      simpl. rewrite <- Heql.
      rewrite replace_preserves_Zlength. assumption.
      Transparent Z.add Z.of_nat.
  Qed.

  Lemma ioapic_init_max_intr_within_range:
    ∀ d,
      0 ≤ IoApicMaxIntr (s (ioapic d)) < 32 →
      0 ≤
      IoApicMaxIntr
        (ioapic_init_aux (s (ioapic d))
                         (Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))) < 32.
  Proof.
    intros. calc. rewrite init_does_not_change_max_intr. assumption.
  Qed.

  Lemma ioapic_init_does_not_change_enables_length:
    ∀ d,
      Zlength (IoApicEnables (s (ioapic d))) = IoApicMaxIntr (s (ioapic d)) + 1 →
      Zlength (IoApicEnables (ioapic_init_aux (s (ioapic d)) (Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1)))) =
      IoApicMaxIntr (ioapic_init_aux (s (ioapic d)) (Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))) + 1.
  Proof.
    intros d.
    rewrite init_does_not_change_max_intr.
    rewrite init_does_not_change_enables_length.
    auto.
  Qed.

  Lemma ioapic_init_does_not_change_irqs_length:
    ∀ d,
      Zlength (IoApicIrqs (s (ioapic d))) = IoApicMaxIntr (s (ioapic d)) + 1 →
      Zlength (IoApicIrqs (ioapic_init_aux (s (ioapic d)) (Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1)))) =
      IoApicMaxIntr (ioapic_init_aux (s (ioapic d)) (Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))) + 1.
  Proof.
    intros d.
    rewrite init_does_not_change_max_intr.
    rewrite init_does_not_change_irqs_length.
    auto.
  Qed.

  Lemma ioapic_trans_intr_does_not_change_enables_length:
    ∀ d irq,
      Zlength (IoApicEnables (s (ioapic d))) = IoApicMaxIntr (s (ioapic d)) + 1 →
      Zlength (IoApicEnables (ioapic_trans_intr irq (s (ioapic d)))) =
      IoApicMaxIntr (ioapic_trans_intr irq (s (ioapic d))) + 1.
  Proof.
    intros d irq H.
    rewrite ioapic_trans_intr_reserves_maxintr_simpl.
    rewrite ioapic_trans_intr_reserves_enables_length_simpl.
    assumption.
  Qed.

  Lemma ioapic_trans_intr_does_not_change_irqs_length:
    ∀ d irq,
      Zlength (IoApicIrqs (s (ioapic d))) = IoApicMaxIntr (s (ioapic d)) + 1 →
      Zlength (IoApicIrqs (ioapic_trans_intr irq (s (ioapic d)))) =
      IoApicMaxIntr (ioapic_trans_intr irq (s (ioapic d))) + 1.
  Proof.
    intros d irq H.
    rewrite ioapic_trans_intr_reserves_maxintr_simpl.
    rewrite ioapic_trans_intr_reserves_irqs_length_simpl.
    assumption.
  Qed.

  Lemma ioapic_trans_cpu_does_not_change_enables_length:
    ∀ d op,
      Zlength (IoApicEnables (s (ioapic d))) = IoApicMaxIntr (s (ioapic d)) + 1 →
      Zlength (IoApicEnables (ioapic_trans_cpu op (s (ioapic d)))) =
      IoApicMaxIntr (ioapic_trans_cpu op (s (ioapic d))) + 1.
  Proof.
    intros d op H.
    rewrite ioapic_trans_cpu_reserves_maxintr_simpl.
    rewrite ioapic_trans_cpu_reserves_enables_length_simpl.
    assumption.
  Qed.

  Lemma ioapic_trans_cpu_does_not_change_irqs_length:
    ∀ d op,
      Zlength (IoApicIrqs (s (ioapic d))) = IoApicMaxIntr (s (ioapic d)) + 1 →
      Zlength (IoApicIrqs (ioapic_trans_cpu op (s (ioapic d)))) =
      IoApicMaxIntr (ioapic_trans_cpu op (s (ioapic d))) + 1.
  Proof.
    intros d op H.
    rewrite ioapic_trans_cpu_reserves_maxintr_simpl.
    rewrite ioapic_trans_cpu_reserves_irqs_length_simpl.
    assumption.
  Qed.

End IOAPIC_INV.

Hint Resolve handle_cons_buf_write_reserve_rpos.
Hint Resolve handle_cons_buf_write_reserve_cons_buf_len.

Hint Resolve cons_buf_plus_1_reserve_rpos.
Hint Resolve cons_buf_tl_cons_reserve_cons_buf_len.
Hint Resolve cons_intr_preserves_cons_buf_len.
Hint Resolve cons_intr_preserves_rpos_range.
Hint Resolve cons_intr_skipn_reserve_cons_buf_len.

Hint Resolve nil_zlength_within_range.
Hint Resolve ioapic_trans_intr_reserves_maxintr_within_range.
Hint Resolve ioapic_trans_cpu_reserves_maxintr_within_range.
Hint Resolve ioapic_init_max_intr_within_range.
Hint Resolve ioapic_init_does_not_change_enables_length.
Hint Resolve ioapic_init_does_not_change_irqs_length.
Hint Resolve ioapic_trans_intr_does_not_change_enables_length.
Hint Resolve ioapic_trans_intr_does_not_change_irqs_length.
Hint Resolve ioapic_trans_cpu_does_not_change_enables_length.
Hint Resolve ioapic_trans_cpu_does_not_change_irqs_length.