Module AbMachineEnv

Proof.

    induction me; simpl; intros H q Hq; inv Hq; econstructor (eauto).
    specialize (H _ eq_refl). easy.
  Qed.

Proof.

    destruct 1.
    - destruct H0; constructor.
    - destruct n; constructor.
    - destruct H0; constructor.
    - destruct H1; try constructor; simpl;
      match goal with |- context [of_bool ?b] => destruct b end; constructor.
  Qed.

  Definition me_const_i (i: int) : mexpr := MEconst (MNint i).
  Definition me_const_l (i: int64) : mexpr := MEconst (MNint64 i).
  Definition me_const_f (f: float) : mexpr := MEconst (MNfloat f).
  Definition me_const_s (f: float32) : mexpr := MEconst (MNsingle f).

End mexpr.

Inductive mach_num_itv : Type :=
| MNIint : zitv+⊤ -> mach_num_itv
| MNIint64 : zitv+⊤ -> mach_num_itv
| MNIfloat : fitv+⊤ -> mach_num_itv
| MNIsingle : fitv+⊤ -> mach_num_itv.

Inductive mach_num_itv_gamma : gamma_op mach_num_itv mach_num :=
| MNIint_ok : ∀ itv i,
    i ∈ γ itv -> mach_num_itv_gamma (MNIint itv) (MNint (Int.repr i))
| MNIint64_ok : ∀ itv i,
    i ∈ γ itv -> mach_num_itv_gamma (MNIint64 itv) (MNint64 (Int64.repr i))
| MNIfloat_ok : ∀ itv f,
    f ∈ γ itv ->
    mach_num_itv_gamma (MNIfloat itv) (MNfloat f)
| MNIsingle_ok : ∀ itv f,
    Float.of_single f ∈ γ itv ->
    mach_num_itv_gamma (MNIsingle itv) (MNsingle f).
Existing Instance mach_num_itv_gamma.

Unset Elimination Schemes.

Domain of environments using machine numbers.

Class ab_machine_env (var t iter_t: Type) `{EqDec var} : Type := {
  mach_top:> top_op (t+⊥);
  mach_leb:> leb_op t;
  mach_join:> join_op t (t+⊥);
  mach_widen:> widen_op iter_t (t+⊥);

  assign: var -> mexpr var -> t -> t+⊥;
  forget: var -> t -> t+⊥;
  assume: mexpr var -> bool -> t -> t+⊥;
  get_itv: mexpr var -> t -> mach_num_itv+⊥;
  concretize_int: N -> mexpr var -> t -> ZSet.t+⊤+⊥;
  noerror: mexpr var -> t -> bool;

  mach_gamma:> gamma_op t (var -> mach_num);
  mach_gamma_iter:> gamma_op iter_t (var -> mach_num);

  mach_top_correct:> top_op_correct (t+⊥) (var -> mach_num);
  mach_leb_correct:> leb_op_correct t (var -> mach_num);
  mach_join_correct:> join_op_correct t (t+⊥) (var -> mach_num);
  mach_widen_correct:> widen_op_correct iter_t (t+⊥) (var -> mach_num);
  assign_correct: ∀ x e ρ n ab,
    ρ ∈ γ ab ->
    n ∈ eval_mexpr ρ e ->
    ρ +[x => n] ∈ γ (assign x e ab);
  forget_correct: ∀ x ρ n ab,
    ρ ∈ γ ab ->
    ρ +[x => n] ∈ γ (forget x ab);
  assume_correct: ∀ e ρ ab b,
    ρ ∈ γ ab ->
    of_bool b ∈ eval_mexpr ρ e ->
    ρ ∈ γ (assume e b ab);
  get_itv_correct: ∀ e ρ ab,
    ρ ∈ γ ab ->
    (eval_mexpr ρ e) ⊆ γ (get_itv e ab);
  concretize_int_correct: ∀ n e ρ ab,
    ρ ∈ γ ab ->
    (eval_mexpr ρ e ∘ MNint) ⊆ γ (concretize_int n e ab);
  noerror_correct: ∀ e ρ ab,
    ρ ∈ γ ab ->
    noerror e ab = true ->
    error_mexpr ρ e ->
    False
}.

Section MORE.

Context (var t iter_t: Type) `(EQ: EqDec var) `(D: @ab_machine_env var t iter_t EQ).

Lemma forget_correct':
  ∀ (x: var) (ρ ρ': var → mach_num) (ab: t),
    ρ ∈ γ(ab) →
    (∀ y, y ≠ x → ρ'(y) = ρ(y)) →
    ρ' ∈ γ (forget x ab).

Proof.

  intros x ρ ρ' ab H3 H2.
  erewrite (Axioms.extensionality ρ').
  apply forget_correct; eauto.
  intros z. unfold upd.
  destruct @eq_dec as [ -> | ME ]. reflexivity.
  apply H2, ME.
Qed.

Lemma assume_bot:
  ∀ e b (ab: t),
    is_bot (assume e b ab) = true →
    ∀ ρ, ρ ∈ γ(ab) →
         ¬ of_bool(b) ∈ eval_mexpr ρ e.

Proof.

  intros e b ab B ρ G K.
  erewrite is_bot_spec in B. discriminate.
  apply assume_correct; eauto.
Qed.

Definition is_null (ab: t) (me: mexpr var) : bool :=
  is_bot (assume (MEbinop (Ocmpu Ceq) me (me_const_i _ Int.zero)) false ab).

Lemma is_null_correct (ab: t) ρ (G: ρ ∈ γ ab) me :
  is_null ab me = true →
  ∀ i, MNint i ∈ eval_mexpr ρ me → i = Int.zero.

Proof.

  unfold is_null.
  intros N i Hi. generalize (assume_bot false ab N G). clear N.
  simpl. intros K.
  destruct (Int.cmpu Ceq i Int.zero) eqn: Hz.
  simpl in Hz. generalize (Int.eq_spec i Int.zero). rewrite Hz. exact id.
  elim K. econstructor; eauto. vauto.
  change Nfalse with (of_bool false). rewrite <- Hz. vauto.
Qed.

End MORE.