Module AbIdealNonrel

Require Import Coqlib Utf8 Util AdomLib FastArith.
Require Import Floats IdealExpr ZIntervals AbIdealEnv.

Set Implicit Arguments.

Unset Elimination Schemes.
Class ab_ideal_nonrel (t:Type) : Type :=
{ as_leb :> leb_op t
; as_join :> join_op t (t+⊤)
; as_meet :> meet_op t (t+⊥)
; widen : t -> t -> t+⊤

; const: ideal_num -> t+⊤
; z_itv: zitv -> t+⊤

; forward_unop: i_unary_operation -> t+⊤ -> t+⊤+⊥
; forward_binop: i_binary_operation -> t+⊤ -> t+⊤ -> t+⊤+⊥

; backward_unop: i_unary_operation -> t+⊤ -> t+⊤ -> t+⊤+⊥
; backward_binop: i_binary_operation -> t+⊤ -> t+⊤ -> t+⊤ -> (t+⊤*t+⊤)+⊥

; forward_expr_evaluator := iexpr -> t+⊤+⊥
; backward_expr_evaluator (AB:Type) := iexpr -> t -> AB * query_chan -> AB+⊥
; var_refiner (AB:Type) := t -> AB -> AB+⊥

; forward_var: forward_expr_evaluator -> var -> t+⊤ -> query_chan -> t+⊤+⊥
; backward_var: forward_expr_evaluator -> ∀ {AB},
                backward_expr_evaluator AB ->
                var_refiner AB ->
                var -> t -> AB * query_chan -> AB+⊥

; enrich_query_chan: forward_expr_evaluator -> query_chan -> query_chan

; process_msg: forward_expr_evaluator -> ∀ {AB}, backward_expr_evaluator AB ->
               message -> AB * query_chan -> (AB*messages_chan)+⊥
; assign_msgs : var -> t -> messages_chan
; assume_msgs : var -> t+⊤ -> t -> messages_chan

}.

Class ab_ideal_nonrel_correct t (D: ab_ideal_nonrel t) (G:gamma_op t ideal_num) : Prop :=
{ join_idem: ∀ x : t, join x x = Just x
; widen_idem: ∀ x : t, widen x x = Just x
; leb_refl: ∀ x : t, leb x x = true

; as_leb_correct :> leb_op_correct t ideal_num
; as_join_correct :> join_op_correct t (t+⊤) ideal_num
; as_meet_correct :> meet_op_correct t (t+⊥) ideal_num
; widen_incr: ∀ x y, γ x ⊆ γ (widen x y)

; const_correct: ∀ n, n ∈ γ (const n)
; z_itv_correct: ∀ (i:zitv) (z:Z), z ∈ γ i -> (γ (z_itv i) (INz z))
; forward_unop_sound: ∀ op x x_ab, x ∈ γ x_ab ->
    eval_iunop op x ⊆ γ (forward_unop op x_ab)
; forward_binop_sound: ∀ op x x_ab, x ∈ γ x_ab -> ∀ y y_ab, y ∈ γ y_ab ->
    eval_ibinop op x y ⊆ γ (forward_binop op x_ab y_ab)

; backward_unop_sound:
    ∀ op x x_ab, x ∈ γ x_ab -> ∀ res res_ab, res ∈ γ res_ab ->
      eval_iunop op x res ->
      x ∈ γ (backward_unop op res_ab x_ab)

; backward_binop_sound:
    ∀ op x x_ab, x ∈ γ x_ab ->
    ∀ y y_ab, y ∈ γ y_ab ->
    ∀ res res_ab, res ∈ γ res_ab ->
      eval_ibinop op x y res ->
      (x, y) ∈ γ (backward_binop op res_ab x_ab y_ab)

; forward_expr_evaluator_sound ρ (ev:forward_expr_evaluator) :=
    ∀ e v, eval_iexpr ρ e v -> v ∈ γ (ev e)

; backward_expr_evaluator_sound (AB:Type) {GAB:gamma_op AB (var -> ideal_num)}
                                ρ (bev:backward_expr_evaluator AB) :=
    ∀ e v abv ab, eval_iexpr ρ e v -> v ∈ γ abv -> ρ ∈ γ ab -> ρ ∈ γ (bev e abv ab)

; var_refiner_sound (AB:Type) {GAB:gamma_op AB (var -> ideal_num)}
                    ρ (var_ref:var_refiner AB) (x:var) :=
    ∀ abv ab, ρ x ∈ γ abv -> ρ ∈ γ ab -> ρ ∈ γ (var_ref abv ab)

; forward_var_sound:
    ∀ fev x ab c ρ,
      forward_expr_evaluator_sound ρ fev ->
      ρ x ∈ γ ab -> ρ ∈ γ c -> ρ x ∈ γ (forward_var fev x ab c)

; backward_var_sound:
    ∀ fev AB {GAB:gamma_op AB (var -> ideal_num)} bev var_ref x ab abenv ρ,
      forward_expr_evaluator_sound ρ fev ->
      backward_expr_evaluator_sound AB _ ρ bev ->
      var_refiner_sound AB _ ρ var_ref x ->
      ρ x ∈ γ ab -> ρ ∈ γ abenv ->
      ρ ∈ γ (backward_var fev bev var_ref x ab abenv)

; enrich_query_chan_sound:
    ∀ fev c ρ,
      forward_expr_evaluator_sound ρ fev ->
      ρ ∈ γ c -> ρ ∈ γ (enrich_query_chan fev c)

; process_msg_sound:
    ∀ fev AB {GAB:gamma_op AB (var -> ideal_num)} bev msg abenv ρ,
      forward_expr_evaluator_sound ρ fev ->
      backward_expr_evaluator_sound AB _ ρ bev ->
      ρ ∈ γ msg -> ρ ∈ γ abenv -> ρ ∈ γ (process_msg fev bev msg abenv)

; assign_msgs_sound:
    ∀ x v ρ, ρ x ∈ γ v -> ρ ∈ γ (assign_msgs x v)

; assume_msgs_sound:
    ∀ x vOld vNew ρ, ρ x ∈ γ vOld -> ρ x ∈ γ vNew -> ρ ∈ γ (assume_msgs x vOld vNew)
}.