Module CsharpminorAnalysisproof

Require Import CsharpminorAnalysis CsharpminorIterproof MemCsharpminorproof.
Import
  Utf8
  Coqlib Behaviors Csharpminorannot
  DomKind
  Util AbMemSignatureCsharpminor DebugAbMemCsharpminor.

Section VA.

  Context (kind: num_dom_kind)
          (max_concretize: N)
          (trace verbose: bool)
          (unroll: nat).

  Let vanalysis := vanalysis kind max_concretize trace verbose unroll.

  Theorem vanalysis_correct :
    forall prog log, vanalysis prog = (tt, (nil, log)) ->
    forall tr, program_behaves (semantics prog) (Goes_wrong tr) ->
    False.

Proof.

    unfold vanalysis, doit. intros prog log.
    destruct kind, trace, verbose;
    intros; eapply iter_program_sound; eauto;
    match goal with
      | |- mem_dom_spec _ _ (debug_mem_dom _ _) _ _ => eapply debug_mem_dom_sound
      | _ => idtac
    end;
    eapply mem_cshm_dom_correct.
  Qed.

  Local Notation "⟦ p ⟧" := (program_behaves (semantics p)).

  Corollary vanalysis_sound:
    ∀ p log, vanalysis p = (tt, (nil, log)) →
         ⟦p⟧ ⊆ not_wrong.

Proof.

    intros p log H (); try easy.
    intros t H0. exact (vanalysis_correct p log H _ H0).
  Qed.

End VA.