Library liblayers.compcertx.SimCop

Require Import LogicalRelations.
Require Import SimulationRelation.
Require Import OptionOrders.
Require Import Cop.
Require Import SimValues.


Instance flex_option_le_true {A B} (R: rel A B):
  Related (option_le R) (flex_option_le True R) subrel.
Proof.
  destruct 1; constructor; eauto.
Qed.

Section COP_MONOTONIC.
  Context `{Hmem: BaseMemoryModel}.
  Context {D1 D2} (R: simrel D1 D2).

  Global Instance bool_val_match p:
    Monotonic
      Cop.bool_val
      (match_val R p ++> - ==> match_mem R p ++> option_le eq).
  Proof.
    unfold bool_val.
    rewrite !weak_valid_pointer_eq.
    repeat rstep.
  Qed.

  Global Instance: Params (@Cop.bool_val) 3.

  Global Instance sem_switch_arg_match p:
    Monotonic
      (@Cop.sem_switch_arg)
      (match_val R p ++> - ==> simrel_option_le R eq).
  Proof.
    unfold Cop.sem_switch_arg.
    rauto.
  Qed.

  Global Instance sem_unary_operation_match p:
    Monotonic
      Cop.sem_unary_operation
      (- ==> match_val R p ++> - ==> match_mem R p ==> option_le (match_val R p)).
  Proof.
    unfold Cop.sem_unary_operation,
    Cop.sem_notbool,
    Cop.sem_notint,
    Cop.sem_absfloat,
    Cop.sem_neg.
    clear.     solve_monotonic.
    congruence.
  Qed.

  Global Instance: Params (@Cop.sem_unary_operation) 4.

  Global Instance sem_cast_match p:
    Monotonic
      Cop.sem_cast
      (match_val R p ++> - ==> - ==> match_mem R p ++>
       option_le (match_val R p)).
  Proof.
    unfold Cop.sem_cast.
    clear.     rewrite !weak_valid_pointer_eq.
    solve_monotonic.
    - rdestruct_assert; [ apply eq_refl | rauto ].     - rdestruct_assert; [ apply eq_refl | rauto ].   Qed.

  Global Instance: Params (@Cop.sem_cast) 4.

  Local Instance simrel_option_le_subrel {A B: Type} (RAB: rel A B):
    Related
      (simrel_option_le R RAB)
      (option_le RAB)
      subrel.
  Proof.
    intros o1 o2 Ho.
    inversion Ho; constructor; auto.
  Qed.

  Lemma match_ptrbits_shift_sub p b1 ofs1 b2 ofs2 delta:
    match_ptrbits R p (b1, ofs1) (b2, ofs2) →
    match_ptrbits R p (b1, Ptrofs.sub ofs1 delta) (b2, Ptrofs.sub ofs2 delta).
  Proof.
    rewrite !Ptrofs.sub_add_opp.
    apply match_ptrbits_shift.
  Qed.

  Global Instance sem_binarith_match p:
    Monotonic
      Cop.sem_binarith
      ((- ==> - ==> - ==> option_le (match_val R p)) ++>
       (- ==> - ==> - ==> option_le (match_val R p)) ++>
       (- ==> - ==> option_le (match_val R p)) ++>
       (- ==> - ==> option_le (match_val R p)) ++>
       match_val R p ++> - ==>
       match_val R p ++> - ==>
       match_mem R p ++>
       option_le (match_val R p)).
  Proof.
    unfold Cop.sem_binarith.
    clear.     solve_monotonic.
  Qed.

  Global Instance: Params (@Cop.sem_binarith) 9.

  Remove Hints funext_mor4 : typeclass_instances.

  Global Instance cmp_ptr_match p:
    Related
      (@Cop.cmp_ptr (mwd D1) Mem.valid_pointer)
      (@Cop.cmp_ptr (mwd D2) Mem.valid_pointer)
      (match_mem R p ++> - ==> match_val R p ++> match_val R p ++>
       option_le (match_val R p)).
  Proof.
    unfold cmp_ptr.
    rauto.
  Qed.

  Global Instance: Params (@cmp_ptr) 4.

  Global Instance sem_cmp_match p:
    Monotonic
     Cop.sem_cmp
     (- ==>
      match_val R p ++> - ==>
      match_val R p ++> - ==>
      match_mem R p ++>
       option_le (match_val R p)).
  Proof.
    unfold sem_cmp.
    solve_monotonic.
  Qed.

  Global Instance: Params (@Cop.sem_cmp) 6.

  Global Instance sem_shift_match p:
    Monotonic
      Cop.sem_shift
      (- ==>
       - ==>
       match_val R p ++> - ==>
       match_val R p ++> - ==>
       option_le (match_val R p)).
  Proof.
    unfold Cop.sem_shift.
    clear.     solve_monotonic.
  Qed.

  Global Instance: Params (@Cop.sem_shift) 6.

  Global Instance sem_binary_operation_match p:
    Monotonic
      Cop.sem_binary_operation
      (- ==> - ==>
       match_val R p ++> - ==>
       match_val R p ++> - ==>
       match_mem R p ++>
       option_le (match_val R p)).
  Proof.
    unfold Cop.sem_binary_operation.
    unfold
    sem_add,
    sem_add_ptr_int,
    sem_add_ptr_long,
    sem_sub,
    sem_mul,
    sem_div,
    sem_mod,
    sem_and,
    sem_or,
    sem_xor,
    sem_shl,
    sem_shr.
    solve_monotonic;
      auto using match_ptrbits_shift, match_ptrbits_shift_sub.
    - destruct b4; try rauto.
      assert (Ptrofs.sub ofs1 ofs0 = Ptrofs.sub ofs2 ofs3).
      {
        subst.
        inv H4; inv H5.
        replace delta0 with delta in × by congruence.
        symmetry.
        apply Ptrofs.sub_shifted.
      }
      pose proof BoolRel.andb_leb.       repeat rstep; congruence.
  Qed.

  Global Instance: Params (@Cop.sem_binary_operation) 7.
End COP_MONOTONIC.