Module MoreSemantics

Require Import Behaviors.
Require Import Util.
Import Utf8.
Import Coqlib.
Import Smallstep.

Lemma forall_exists {T: Type} (P : T → Prop) : (∀ t : T, ¬ P t) ∨ ∃ t : T, P t.

Section SEM.

Context (sem: semantics).

Definition reachable (s: state sem) : Prop :=
  ∃ i tr, initial_state sem i ∧ star (step sem) (globalenv sem) i tr s.

Lemma reachable_initial_state { s } :
  s ∈ initial_state sem →
  s ∈ reachable.

Lemma reachable_step {s tr s'} :
  step sem (globalenv sem) s tr s' →
  reachable s →
  reachable s'.

Lemma reachable_star {s tr s'} :
  Star sem s tr s' →
  reachable s →
  reachable s'.

Lemma reachable_plus {s tr s'} :
  Plus sem s tr s' →
  reachable s →
  reachable s'.

Definition invariant (P: state sem → Prop) : Prop :=
  reachable ⊆ P.

Definition invariant_weaken (P Q: state sem → Prop) :
  (P ⊆ Q) → invariant P → invariant Q :=
  λ w p s r, w s (p s r).

Definition safe : Prop :=
  program_behaves sem ⊆ not_wrong.

Section INVARIANT.

Context (P: state sem → Prop).

Hypothesis invariant_init : initial_state sem ⊆ P.

Hypothesis invariant_step :
  ∀ s, reachable s → P s → ∀ tr, step sem (globalenv sem) s tr ⊆ P.

Theorem invariant_ind: invariant P.

End INVARIANT.

Context P (Hinv: invariant P).

Definition sem_with_strong_local_invariant : semantics :=
  {|
    state := state sem;
    genvtype := genvtype sem;
    step := λ ge s tr s', step sem ge s tr s' ∧ P s';
    initial_state := initial_state sem ∩ P;
    final_state := final_state sem;
    globalenv := globalenv sem;
    symbolenv := symbolenv sem
  |}.

Theorem global_invariant_strong_local :
  forward_simulation sem sem_with_strong_local_invariant.

Definition sem_with_local_invariant : semantics :=
  {|
    state := state sem;
    genvtype := genvtype sem;
    step := λ ge s tr s', step sem ge s tr s' ∧ P s;
    initial_state := initial_state sem;
    final_state := final_state sem;
    globalenv := globalenv sem;
    symbolenv := symbolenv sem
  |}.

Theorem global_invariant_local :
  forward_simulation sem sem_with_local_invariant.

Lemma blocking_determinate :
  determinate sem →
  determinate sem_with_local_invariant.

End SEM.

Definition behavior_inclusion_preserves_safety (L1 L2: semantics) :
  program_behaves L2 ⊆ program_behaves L1 →
  safe L1 → safe L2 :=
  λ i s b H, s b (i b H).

Lemma strong_local_invariant_global' sem P :
  invariant (sem_with_strong_local_invariant sem P) P.

Lemma safe_progress {sem} :
  safe sem →
  ∀ {s}, reachable sem s →
       (∃ tr s', step sem (globalenv sem) s tr s') ∨ (∃ r, final_state sem s r).

Lemma local_invariant_global_1 sem P :
  safe (sem_with_local_invariant sem P) →
  invariant (sem_with_local_invariant sem P) (P ∪ λ s, ∃ r, final_state sem s r).

Lemma local_invariant_global_2 sem P :
  (∀ r s, final_state sem s r → Nostep sem s) →
  safe (sem_with_local_invariant sem P) →
  invariant sem (reachable (sem_with_local_invariant sem P)).

Theorem local_invariant_global sem P :
  (∀ r s, final_state sem s r → Nostep sem s) →
  safe (sem_with_local_invariant sem P) →
  invariant sem (P ∪ λ s, ∃ r, final_state sem s r).

Section SIM.

Context {L1 L2: semantics} (sim: forward_simulation L1 L2).

Lemma reachable_sim s1 :
  reachable L1 s1 →
  ∃ idx s2,
    reachable L2 s2 ∧ fsim_match_states sim idx s1 s2.

End SIM.

Section BSIM.

Context {L1 L2: semantics} (sim: backward_simulation L1 L2).
Context (DET: ∀ r s, final_state L2 s r → Nostep L2 s).

Context (P1: state L1 → Prop) (P2: state L2 → Prop).

Hypothesis L1_safe : safe L1.

Hypothesis inv1 : invariant L1 P1.

Hypothesis inv2_from_sim :
  ∀ idx s1 s2,
    sim idx s1 s2 →
    s1 ∈ P1 →
    s2 ∈ P2.

Lemma invariant_from_match_state: invariant L2 (P2 ∪ λ s, ∃ r, final_state L2 s r).

End BSIM.